# HG changeset patch
# User wenzelm
# Date 1483362873 -3600
# Node ID 2450b62574c6975e4591a465feb2eda52db21946
# Parent  155bf86321041d2006ad8fbb1f93ee624276ba79
grammar for Isabelle/ML, based on https://github.com/textmate/standard-ml.tmbundle/blob/fea2448/Syntaxes/Standard%20ML.plist

diff -r 155bf8632104 -r 2450b62574c6 src/Tools/VSCode/extension/isabelle-ml-grammar.json
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/isabelle-ml-grammar.json	Mon Jan 02 14:14:33 2017 +0100
@@ -0,0 +1,288 @@
+{
+  "name": "Isabelle/ML",
+  "scopeName": "source.isabelle-ml",
+  "fileTypes": ["ML"],
+  "uuid": "aa32eb5e-d0d9-11e6-b7a4-37ba001f1e6e",
+  "keyEquivalent": "^~M",
+  "repository": {
+    "comments": {
+      "patterns": [
+        {
+          "end": "\\*\\)",
+          "begin": "\\(\\*",
+          "beginCaptures": {
+            "0": {
+              "name": "punctuation.definition.comment.begin.ml"
+            }
+          },
+          "patterns": [
+            {
+              "include": "#comments"
+            }
+          ],
+          "endCaptures": {
+            "0": {
+              "name": "punctuation.definition.comment.end.ml"
+            }
+          },
+          "name": "comment.block.ml"
+        }
+      ]
+    },
+    "spec": {
+      "patterns": [
+        {
+          "match": "\\b(exception|type)\\s+([a-zA-Z][a-zA-Z0-9'_]*)",
+          "captures": {
+            "1": {
+              "name": "keyword.other.ml"
+            },
+            "2": {
+              "name": "entity.name.type.abbrev.ml"
+            }
+          },
+          "name": "meta.spec.ml.type"
+        },
+        {
+          "end": "(?=val|type|eqtype|datatype|structure|include|exception)",
+          "begin": "\\b(datatype)\\s+([a-zA-Z][a-zA-Z0-9'_]*)\\s*(?==)",
+          "patterns": [
+            {
+              "match": "\\b(and)\\s+([a-zA-Z][a-zA-Z0-9'_]*)\\s*(?==)",
+              "captures": {
+                "1": {
+                  "name": "keyword.other.ml"
+                },
+                "2": {
+                  "name": "entity.name.type.datatype.ml"
+                }
+              },
+              "name": "meta.spec.ml.datatype"
+            },
+            {
+              "match": "(?x)\n\t\t\t\t\t\t\t=\\s*([a-zA-Z][a-zA-Z0-9'_]*)(\\s+of)?",
+              "captures": {
+                "1": {
+                  "name": "variable.other.dcon.ml"
+                },
+                "2": {
+                  "name": "keyword.other.ml"
+                }
+              },
+              "name": "meta.datatype.rule.main.ml"
+            },
+            {
+              "match": "\\|\\s*([a-zA-Z][a-zA-Z0-9'_]*)(\\s+of)?",
+              "captures": {
+                "1": {
+                  "name": "variable.other.dcon.ml"
+                },
+                "2": {
+                  "name": "keyword.other.ml"
+                }
+              },
+              "name": "meta.datatype.rule.other.ml"
+            }
+          ],
+          "captures": {
+            "1": {
+              "name": "keyword.other.ml"
+            },
+            "2": {
+              "name": "entity.name.type.datatype.ml"
+            }
+          },
+          "name": "meta.spec.ml.datatype"
+        },
+        {
+          "match": "\\b(val)\\s*([^:]+)\\s*:",
+          "captures": {
+            "1": {
+              "name": "keyword.other.ml"
+            }
+          },
+          "name": "meta.spec.ml.val"
+        },
+        {
+          "end": "(?=val|type|eqtype|datatype|structure|include)",
+          "begin": "\\b(structure)\\s*(\\w+)\\s*:",
+          "patterns": [
+            {
+              "match": "\\b(sharing)\\b",
+              "name": "keyword.other.ml"
+            }
+          ],
+          "captures": {
+            "1": {
+              "name": "keyword.other.ml"
+            },
+            "2": {
+              "name": "entity.name.type.module.ml"
+            }
+          },
+          "name": "meta.spec.ml.structure"
+        },
+        {
+          "match": "\\b(include)\\b",
+          "captures": {
+            "1": {
+              "name": "keyword.other.ml"
+            }
+          },
+          "name": "meta.spec.ml.include"
+        },
+        {
+          "include": "#comments"
+        }
+      ]
+    }
+  },
+  "patterns": [
+    {
+      "include": "#comments"
+    },
+    {
+      "match": "\\b(val|datatype|signature|type|op|sharing|struct|as|let|in|abstype|local|where|case|of|fn|raise|exception|handle|ref|infix|infixr|before|end|structure|withtype)\\b",
+      "name": "keyword.other.ml"
+    },
+    {
+      "end": "\\b(end)\\b",
+      "begin": "\\b(let)\\b",
+      "patterns": [
+        {
+          "include": "$self"
+        }
+      ],
+      "captures": {
+        "1": {
+          "name": "keyword.other.ml"
+        },
+        "2": {
+          "name": "keyword.other.ml"
+        }
+      },
+      "name": "meta.exp.let.ml"
+    },
+    {
+      "end": "\\b(end)\\b",
+      "begin": "\\b(sig)\\b",
+      "patterns": [
+        {
+          "include": "#spec"
+        }
+      ],
+      "captures": {
+        "1": {
+          "name": "keyword.other.delimiter.ml"
+        },
+        "2": {
+          "name": "keyword.other.delimiter.ml"
+        }
+      },
+      "name": "meta.module.sigdec.ml"
+    },
+    {
+      "match": "\\b(if|then|else)\\b",
+      "name": "keyword.control.ml"
+    },
+    {
+      "end": "(?=val|type|eqtype|datatype|structure|local)",
+      "begin": "\\b(fun|and)\\s+([\\w]+)\\b",
+      "patterns": [
+        {
+          "include": "source.ml"
+        }
+      ],
+      "captures": {
+        "1": {
+          "name": "keyword.control.fun.ml"
+        },
+        "2": {
+          "name": "entity.name.function.ml"
+        }
+      },
+      "name": "meta.definition.fun.ml"
+    },
+    {
+      "end": "\"",
+      "begin": "\"",
+      "beginCaptures": {
+        "0": {
+          "name": "punctuation.definition.string.begin.ml"
+        }
+      },
+      "patterns": [
+        {
+          "match": "\\\\.",
+          "name": "constant.character.escape.ml"
+        }
+      ],
+      "endCaptures": {
+        "0": {
+          "name": "punctuation.definition.string.end.ml"
+        }
+      },
+      "name": "string.quoted.double.ml"
+    },
+    {
+      "match": "(#\")(\\\\)?.(\")",
+      "captures": {
+        "3": {
+          "name": "punctuation.definition.constant.ml"
+        },
+        "1": {
+          "name": "punctuation.definition.constant.ml"
+        }
+      },
+      "name": "constant.character.ml"
+    },
+    {
+      "match": "\\b\\d*\\.?\\d+\\b",
+      "name": "constant.numeric.ml"
+    },
+    {
+      "match": "\\b(andalso|orelse|not)\\b",
+      "name": "keyword.operator.logical.ml"
+    },
+    {
+      "end": "(?==|:|\\()",
+      "begin": "(?x)\\b\n\t\t\t\t\t(functor|structure|signature)\\s+\n\t\t\t\t\t(\\w+)\\s* # identifier",
+      "captures": {
+        "1": {
+          "name": "storage.type.module.binder.ml"
+        },
+        "2": {
+          "name": "entity.name.type.module.ml"
+        }
+      },
+      "name": "meta.module.dec.ml"
+    },
+    {
+      "match": "\\b(open)\\b",
+      "name": "keyword.other.module.ml"
+    },
+    {
+      "match": "\\b(nil|true|false|NONE|SOME)\\b",
+      "name": "constant.language.ml"
+    },
+    {
+      "end": "$",
+      "begin": "\\b(type|eqtype) .* =",
+      "patterns": [
+        {
+          "match": "(([a-zA-Z0-9\\.\\* ]|(\\->))*)",
+          "name": "meta.typeexp.ml"
+        }
+      ],
+      "captures": {
+        "1": {
+          "name": "keyword.other.typeabbrev.ml"
+        },
+        "2": {
+          "name": "variable.other.typename.ml"
+        }
+      },
+      "name": "meta.typeabbrev.ml"
+    }
+  ]
+}
\ No newline at end of file
diff -r 155bf8632104 -r 2450b62574c6 src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Mon Jan 02 11:42:15 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json	Mon Jan 02 14:14:33 2017 +0100
@@ -27,13 +27,27 @@
                 "aliases": ["Isabelle"],
                 "extensions": [".thy"],
                 "configuration": "./isabelle-language.json"
+            },
+            {
+                "id": "isabelle-ml",
+                "aliases": ["Isabelle/ML"],
+                "extensions": [".ML"],
+                "configuration": "./isabelle-language.json"
             }
+
         ],
-        "grammars": [{
+        "grammars": [
+            {
                 "language": "isabelle",
                 "scopeName": "source.isabelle",
                 "path": "./isabelle-grammar.json"
-        }],
+            },
+            {
+                "language": "isabelle-ml",
+                "scopeName": "source.isabelle-ml",
+                "path": "./isabelle-ml-grammar.json"
+            }
+        ],
         "configuration": {
             "title": "Isabelle",
             "properties": {