diff options
Diffstat (limited to 'media/CodeMirror-0.62/js/highlight.js')
-rw-r--r-- | media/CodeMirror-0.62/js/highlight.js | 68 |
1 files changed, 0 insertions, 68 deletions
diff --git a/media/CodeMirror-0.62/js/highlight.js b/media/CodeMirror-0.62/js/highlight.js deleted file mode 100644 index f0de59c..0000000 --- a/media/CodeMirror-0.62/js/highlight.js +++ /dev/null @@ -1,68 +0,0 @@ -// Minimal framing needed to use CodeMirror-style parsers to highlight -// code. Load this along with tokenize.js, stringstream.js, and your -// parser. Then call highlightText, passing a string as the first -// argument, and as the second argument either a callback function -// that will be called with an array of SPAN nodes for every line in -// the code, or a DOM node to which to append these spans, and -// optionally (not needed if you only loaded one parser) a parser -// object. - -// Stuff from util.js that the parsers are using. -var StopIteration = {toString: function() {return "StopIteration"}}; - -var Editor = {}; -var indentUnit = 2; - -(function(){ - function normaliseString(string) { - var tab = ""; - for (var i = 0; i < indentUnit; i++) tab += " "; - - string = string.replace(/\t/g, tab).replace(/\u00a0/g, " ").replace(/\r\n?/g, "\n"); - var pos = 0, parts = [], lines = string.split("\n"); - for (var line = 0; line < lines.length; line++) { - if (line != 0) parts.push("\n"); - parts.push(lines[line]); - } - - return { - next: function() { - if (pos < parts.length) return parts[pos++]; - else throw StopIteration; - } - }; - } - - window.highlightText = function(string, callback, parser) { - var parser = (parser || Editor.Parser).make(stringStream(normaliseString(string))); - var line = []; - if (callback.nodeType == 1) { - var node = callback; - callback = function(line) { - for (var i = 0; i < line.length; i++) - node.appendChild(line[i]); - node.appendChild(document.createElement("BR")); - }; - } - - try { - while (true) { - var token = parser.next(); - if (token.value == "\n") { - callback(line); - line = []; - } - else { - var span = document.createElement("SPAN"); - span.className = token.style; - span.appendChild(document.createTextNode(token.value)); - line.push(span); - } - } - } - catch (e) { - if (e != StopIteration) throw e; - } - if (line.length) callback(line); - } -})(); |