X-Git-Url: http://git.onelab.eu/?a=blobdiff_plain;f=third-party%2Fcodemirror-3.15%2Fmode%2Fstex%2Fstex.js;fp=third-party%2Fcodemirror-3.15%2Fmode%2Fstex%2Fstex.js;h=ca04c24f22847fbbc87d63e8751aa59a176cb442;hb=75d3bceb8e1d168e83982f910a916aee3bab7981;hp=0000000000000000000000000000000000000000;hpb=302dd5bda1297ed6579ca26da35ee67f8d35d934;p=unfold.git

diff --git a/third-party/codemirror-3.15/mode/stex/stex.js b/third-party/codemirror-3.15/mode/stex/stex.js
new file mode 100644
index 00000000..ca04c24f
--- /dev/null
+++ b/third-party/codemirror-3.15/mode/stex/stex.js
@@ -0,0 +1,246 @@
+/*
+ * Author: Constantin Jucovschi (c.jucovschi@jacobs-university.de)
+ * Licence: MIT
+ */
+
+CodeMirror.defineMode("stex", function() {
+    "use strict";
+
+    function pushCommand(state, command) {
+        state.cmdState.push(command);
+    }
+
+    function peekCommand(state) {
+        if (state.cmdState.length > 0) {
+            return state.cmdState[state.cmdState.length - 1];
+        } else {
+            return null;
+        }
+    }
+
+    function popCommand(state) {
+        var plug = state.cmdState.pop();
+        if (plug) {
+            plug.closeBracket();
+        }
+    }
+
+    // returns the non-default plugin closest to the end of the list
+    function getMostPowerful(state) {
+        var context = state.cmdState;
+        for (var i = context.length - 1; i >= 0; i--) {
+            var plug = context[i];
+            if (plug.name == "DEFAULT") {
+                continue;
+            }
+            return plug;
+        }
+        return { styleIdentifier: function() { return null; } };
+    }
+
+    function addPluginPattern(pluginName, cmdStyle, styles) {
+        return function () {
+            this.name = pluginName;
+            this.bracketNo = 0;
+            this.style = cmdStyle;
+            this.styles = styles;
+            this.argument = null;   // \begin and \end have arguments that follow. These are stored in the plugin
+
+            this.styleIdentifier = function() {
+                return this.styles[this.bracketNo - 1] || null;
+            };
+            this.openBracket = function() {
+                this.bracketNo++;
+                return "bracket";
+            };
+            this.closeBracket = function() {};
+        };
+    }
+
+    var plugins = {};
+
+    plugins["importmodule"] = addPluginPattern("importmodule", "tag", ["string", "builtin"]);
+    plugins["documentclass"] = addPluginPattern("documentclass", "tag", ["", "atom"]);
+    plugins["usepackage"] = addPluginPattern("usepackage", "tag", ["atom"]);
+    plugins["begin"] = addPluginPattern("begin", "tag", ["atom"]);
+    plugins["end"] = addPluginPattern("end", "tag", ["atom"]);
+
+    plugins["DEFAULT"] = function () {
+        this.name = "DEFAULT";
+        this.style = "tag";
+
+        this.styleIdentifier = this.openBracket = this.closeBracket = function() {};
+    };
+
+    function setState(state, f) {
+        state.f = f;
+    }
+
+    // called when in a normal (no environment) context
+    function normal(source, state) {
+        var plug;
+        // Do we look like '\command' ?  If so, attempt to apply the plugin 'command'
+        if (source.match(/^\\[a-zA-Z@]+/)) {
+            var cmdName = source.current().slice(1);
+            plug = plugins[cmdName] || plugins["DEFAULT"];
+            plug = new plug();
+            pushCommand(state, plug);
+            setState(state, beginParams);
+            return plug.style;
+        }
+
+        // escape characters
+        if (source.match(/^\\[$&%#{}_]/)) {
+          return "tag";
+        }
+
+        // white space control characters
+        if (source.match(/^\\[,;!\/\\]/)) {
+          return "tag";
+        }
+
+        // find if we're starting various math modes
+        if (source.match("\\[")) {
+            setState(state, function(source, state){ return inMathMode(source, state, "\\]"); });
+            return "keyword";
+        }
+        if (source.match("$$")) {
+            setState(state, function(source, state){ return inMathMode(source, state, "$$"); });
+            return "keyword";
+        }
+        if (source.match("$")) {
+            setState(state, function(source, state){ return inMathMode(source, state, "$"); });
+            return "keyword";
+        }
+
+        var ch = source.next();
+        if (ch == "%") {
+            // special case: % at end of its own line; stay in same state
+            if (!source.eol()) {
+              setState(state, inCComment);
+            }
+            return "comment";
+        }
+        else if (ch == '}' || ch == ']') {
+            plug = peekCommand(state);
+            if (plug) {
+                plug.closeBracket(ch);
+                setState(state, beginParams);
+            } else {
+                return "error";
+            }
+            return "bracket";
+        } else if (ch == '{' || ch == '[') {
+            plug = plugins["DEFAULT"];
+            plug = new plug();
+            pushCommand(state, plug);
+            return "bracket";
+        }
+        else if (/\d/.test(ch)) {
+            source.eatWhile(/[\w.%]/);
+            return "atom";
+        }
+        else {
+            source.eatWhile(/[\w\-_]/);
+            plug = getMostPowerful(state);
+            if (plug.name == 'begin') {
+                plug.argument = source.current();
+            }
+            return plug.styleIdentifier();
+        }
+    }
+
+    function inCComment(source, state) {
+        source.skipToEnd();
+        setState(state, normal);
+        return "comment";
+    }
+
+    function inMathMode(source, state, endModeSeq) {
+        if (source.eatSpace()) {
+            return null;
+        }
+        if (source.match(endModeSeq)) {
+            setState(state, normal);
+            return "keyword";
+        }
+        if (source.match(/^\\[a-zA-Z@]+/)) {
+            return "tag";
+        }
+        if (source.match(/^[a-zA-Z]+/)) {
+            return "variable-2";
+        }
+        // escape characters
+        if (source.match(/^\\[$&%#{}_]/)) {
+          return "tag";
+        }
+        // white space control characters
+        if (source.match(/^\\[,;!\/]/)) {
+          return "tag";
+        }
+        // special math-mode characters
+        if (source.match(/^[\^_&]/)) {
+          return "tag";
+        }
+        // non-special characters
+        if (source.match(/^[+\-<>|=,\/@!*:;'"`~#?]/)) {
+            return null;
+        }
+        if (source.match(/^(\d+\.\d*|\d*\.\d+|\d+)/)) {
+          return "number";
+        }
+        var ch = source.next();
+        if (ch == "{" || ch == "}" || ch == "[" || ch == "]" || ch == "(" || ch == ")") {
+            return "bracket";
+        }
+
+        // eat comments here, because inCComment returns us to normal state!
+        if (ch == "%") {
+            if (!source.eol()) {
+                source.skipToEnd();
+            }
+            return "comment";
+        }
+        return "error";
+    }
+
+    function beginParams(source, state) {
+        var ch = source.peek(), lastPlug;
+        if (ch == '{' || ch == '[') {
+            lastPlug = peekCommand(state);
+            lastPlug.openBracket(ch);
+            source.eat(ch);
+            setState(state, normal);
+            return "bracket";
+        }
+        if (/[ \t\r]/.test(ch)) {
+            source.eat(ch);
+            return null;
+        }
+        setState(state, normal);
+        popCommand(state);
+
+        return normal(source, state);
+    }
+
+    return {
+        startState: function() {
+            return {
+                cmdState: [],
+                f: normal
+            };
+        },
+        copyState: function(s) {
+            return {
+                cmdState: s.cmdState.slice(),
+                f: s.f
+            };
+        },
+        token: function(stream, state) {
+            return state.f(stream, state);
+        }
+    };
+});
+
+CodeMirror.defineMIME("text/x-stex", "stex");
+CodeMirror.defineMIME("text/x-latex", "stex");