# HG changeset patch
# User wenzelm
# Date 1483309174 -3600
# Node ID bcdecd466cb2f9de06f3eefc61cf2f723057dc2a
# Parent  9fc965612459786f58c60dae401806cae41b5869
generate static TextMate grammar for VSCode editor;

diff -r 9fc965612459 -r bcdecd466cb2 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Sun Jan 01 23:08:39 2017 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Sun Jan 01 23:19:34 2017 +0100
@@ -114,6 +114,7 @@
       Update_Header.isabelle_tool,
       Update_Then.isabelle_tool,
       Update_Theorems.isabelle_tool,
+      isabelle.vscode.Grammar.isabelle_tool,
       isabelle.vscode.Server.isabelle_tool)
 
   private def list_internal(): List[(String, String)] =
diff -r 9fc965612459 -r bcdecd466cb2 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Jan 01 23:08:39 2017 +0100
+++ b/src/Pure/Tools/build.scala	Sun Jan 01 23:19:34 2017 +0100
@@ -235,8 +235,8 @@
     session_dependencies(options, inlined_files, dirs, List(session))(session)
   }
 
-  def outer_syntax(options: Options, session: String): Outer_Syntax =
-    session_content(options, false, Nil, session).syntax
+  def outer_syntax(options: Options, dirs: List[Path], session: String): Outer_Syntax =
+    session_content(options, false, dirs, session).syntax
 
 
   /* jobs */
diff -r 9fc965612459 -r bcdecd466cb2 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Jan 01 23:08:39 2017 +0100
+++ b/src/Pure/build-jars	Sun Jan 01 23:19:34 2017 +0100
@@ -160,6 +160,7 @@
   ../Tools/Graphview/tree_panel.scala
   ../Tools/VSCode/src/channel.scala
   ../Tools/VSCode/src/document_model.scala
+  ../Tools/VSCode/src/grammar.scala
   ../Tools/VSCode/src/protocol.scala
   ../Tools/VSCode/src/server.scala
   ../Tools/VSCode/src/vscode_rendering.scala
diff -r 9fc965612459 -r bcdecd466cb2 src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Sun Jan 01 23:08:39 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json	Sun Jan 01 23:19:34 2017 +0100
@@ -29,6 +29,11 @@
                 "configuration": "./isabelle-language.json"
             }
         ],
+        "grammars": [{
+                "language": "isabelle",
+                "scopeName": "source.isabelle",
+                "path": "./isabelle-grammar.json"
+        }],
         "configuration": {
             "title": "Isabelle",
             "properties": {
diff -r 9fc965612459 -r bcdecd466cb2 src/Tools/VSCode/src/grammar.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/grammar.scala	Sun Jan 01 23:19:34 2017 +0100
@@ -0,0 +1,154 @@
+/*  Title:      Tools/VSCode/src/grammar.scala
+    Author:     Makarius
+
+Generate static TextMate grammar for VSCode editor.
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+
+object Grammar
+{
+  /* generate grammar */
+
+  private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+
+  private def default_output(logic: String = ""): String =
+    if (logic == default_logic) "isabelle-grammar.json"
+    else "isabelle-" + logic + "-grammar.json"
+
+  def generate(
+    options: Options,
+    session_dirs: List[Path] = Nil,
+    session_name: String = default_logic,
+    output: Path = Path.explode(default_output()))
+  {
+    val keywords = Build.outer_syntax(options, session_dirs, session_name).keywords
+
+    val (minor_keywords, operators) =
+      keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier(_))
+
+    def major_keywords(pred: String => Boolean): List[String] =
+      (for {
+        k <- keywords.major.iterator
+        kind <- keywords.kinds.get(k)
+        if pred(kind)
+      } yield k).toList
+
+    val keywords1 =
+      major_keywords(k => k != Keyword.THY_END && k != Keyword.PRF_ASM && k != Keyword.PRF_ASM_GOAL)
+    val keywords2 = major_keywords(Set(Keyword.THY_END))
+    val keywords3 = major_keywords(Set(Keyword.PRF_ASM, Keyword.PRF_ASM_GOAL))
+
+
+    def quote_name(a: String): String =
+      if (Symbol.is_ascii_identifier(a)) a else "\\Q" + a + "\\E"
+
+    def grouped_names(as: List[String]): String =
+      JSON.Format("\\b(" + as.sorted.map(quote_name(_)).mkString("|") + ")\\b")
+
+    File.write(output, """{
+  "name": "Isabelle",
+  "scopeName": "source.isabelle",
+  "fileTypes": ["thy"],
+  "uuid": "fb16e918-d05b-11e6-918e-2bb94aa2c605",
+  "repository": {
+    "comments": {
+      "patterns": [
+        {
+          "name": "comment.block.isabelle",
+          "begin": "\\(\\*",
+          "beginCaptures": {
+            "0": { "name": "punctuation.definition.comment.begin.isabelle" }
+          },
+          "patterns": [{ "include": "#comments" }],
+          "end": "\\*\\)",
+          "endCaptures": {
+            "0": { "name": "punctuation.definition.comment.end.isabelle" }
+          }
+        }
+      ]
+    }
+  },
+  "patterns": [
+    {
+      "include": "#comments"
+    },
+    {
+      "name": "keyword.control.isabelle",
+      "match": """ + grouped_names(keywords1) + """
+    },
+    {
+      "name": "keyword.other.isabelle",
+      "match": """ + grouped_names(keywords2) + """
+    },
+    {
+      "name": "keyword.operator.isabelle",
+      "match": """ + grouped_names(operators) + """
+    },
+    {
+      "name": "constant.language.isabelle",
+      "match": """ + grouped_names(keywords3) + """
+    },
+    {
+      "match": "\\b\\d*\\.?\\d+\\b",
+      "name": "constant.numeric.isabelle"
+    },
+    {
+      "name": "string.quoted.double.isabelle",
+      "begin": "\"",
+      "beginCaptures": {
+        "0": { "name": "punctuation.definition.string.begin.isabelle" }
+      },
+      "patterns": [
+        {
+          "match": "\\\\.",
+          "name": "constant.character.escape.isabelle"
+        }
+      ],
+      "end": "\"",
+      "endCaptures": {
+        "0": { "name": "punctuation.definition.string.end.isabelle" }
+      }
+    }
+  ]
+}
+""")
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool = Isabelle_Tool("vscode_grammar",
+    "generate static TextMate grammar for VSCode editor", args =>
+  {
+    var dirs: List[Path] = Nil
+    var logic = default_logic
+    var output: Option[Path] = None
+
+    val getopts = Getopts("""
+Usage: isabelle vscode_grammar [OPTIONS]
+
+  Options are:
+    -d DIR       include session directory
+    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
+    -o FILE      output file name (default """ + default_output() + """)
+
+  Generate static TextMate grammar for VSCode editor.
+""",
+      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+      "l:" -> (arg => logic = arg),
+      "o:" -> (arg => output = Some(Path.explode(arg))))
+
+    val more_args = getopts(args)
+    if (more_args.nonEmpty) getopts.usage()
+
+    val output_path = output getOrElse Path.explode(default_output(logic))
+    Output.writeln(output_path.implode)
+
+    generate(Options.init(), dirs, logic, output_path)
+  })
+}