1
0

spanaffectswrapping_shim.html 2.6 KB

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273
  1. <!doctype html>
  2. <html>
  3. <head>
  4. <meta charset="utf-8">
  5. <title>CodeMirror: Automatically derive odd wrapping behavior for your browser</title>
  6. <link rel="stylesheet" href="../doc/docs.css">
  7. </head>
  8. <body>
  9. <h1>CodeMirror: odd wrapping shim</h1>
  10. <p>This is a hack to automatically derive
  11. a <code>spanAffectsWrapping</code> regexp for a browser. See the
  12. comments above that variable
  13. in <a href="../lib/codemirror.js"><code>lib/codemirror.js</code></a>
  14. for some more details.</p>
  15. <div style="white-space: pre-wrap; width: 50px;" id="area"></div>
  16. <pre id="output"></pre>
  17. <script id="script">
  18. var a = document.getElementById("area"), bad = Object.create(null);
  19. var chars = "a~`!@#$%^&*()-_=+}{[]\|'\"/?.>,<:;", l = chars.length;
  20. for (var x = 0; x < l; ++x) for (var y = 0; y < l; ++y) {
  21. var s1 = "foooo" + chars.charAt(x), s2 = chars.charAt(y) + "br";
  22. a.appendChild(document.createTextNode(s1 + s2));
  23. var h1 = a.offsetHeight;
  24. a.innerHTML = "";
  25. a.appendChild(document.createElement("span")).appendChild(document.createTextNode(s1));
  26. a.appendChild(document.createElement("span")).appendChild(document.createTextNode(s2));
  27. if (a.offsetHeight != h1)
  28. bad[chars.charAt(x)] = (bad[chars.charAt(x)] || "") + chars.charAt(y);
  29. a.innerHTML = "";
  30. }
  31. var re = "";
  32. function toREElt(str) {
  33. if (str.length > 1) {
  34. var invert = false;
  35. if (str.length > chars.length * .6) {
  36. invert = true;
  37. var newStr = "";
  38. for (var i = 0; i < l; ++i) if (str.indexOf(chars.charAt(i)) == -1) newStr += chars.charAt(i);
  39. str = newStr;
  40. }
  41. str = str.replace(/[\-\.\]\"\'\\\/\^a]/g, function(orig) { return orig == "a" ? "\\w" : "\\" + orig; });
  42. return "[" + (invert ? "^" : "") + str + "]";
  43. } else if (str == "a") {
  44. return "\\w";
  45. } else if (/[?$*()+{}[\]\.|/\'\"]/.test(str)) {
  46. return "\\" + str;
  47. } else {
  48. return str;
  49. }
  50. }
  51. var newRE = "";
  52. for (;;) {
  53. var left = null;
  54. for (var left in bad) break;
  55. if (left == null) break;
  56. var right = bad[left];
  57. delete bad[left];
  58. for (var other in bad) if (bad[other] == right) {
  59. left += other;
  60. delete bad[other];
  61. }
  62. newRE += (newRE ? "|" : "") + toREElt(left) + toREElt(right);
  63. }
  64. document.getElementById("output").appendChild(document.createTextNode("Your regexp is: " + (newRE || "^$")));
  65. </script>
  66. </body>
  67. </html>