# HG changeset patch
# User wenzelm
# Date 1488891349 -3600
# Node ID 64dfee6bd24333e840254d7ee1126a71f522ec37
# Parent  812c35fbffa8aa2f2f2fc66be6a4c98407a71649
added admin tool "isabelle build_vscode";

diff -r 812c35fbffa8 -r 64dfee6bd243 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Tue Mar 07 10:52:04 2017 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Tue Mar 07 13:55:49 2017 +0100
@@ -117,9 +117,9 @@
       Update_Header.isabelle_tool,
       Update_Then.isabelle_tool,
       Update_Theorems.isabelle_tool,
+      isabelle.vscode.Build_VSCode.isabelle_tool,
       isabelle.vscode.Grammar.isabelle_tool,
-      isabelle.vscode.Server.isabelle_tool,
-      isabelle.vscode.Symbols.isabelle_tool)
+      isabelle.vscode.Server.isabelle_tool)
 
   private def list_internal(): List[(String, String)] =
     for (tool <- internal_tools.toList if tool.accessible)
diff -r 812c35fbffa8 -r 64dfee6bd243 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Mar 07 10:52:04 2017 +0100
+++ b/src/Pure/build-jars	Tue Mar 07 13:55:49 2017 +0100
@@ -160,12 +160,12 @@
   ../Tools/Graphview/popups.scala
   ../Tools/Graphview/shapes.scala
   ../Tools/Graphview/tree_panel.scala
+  ../Tools/VSCode/src/build_vscode.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/symbols.scala
   ../Tools/VSCode/src/vscode_rendering.scala
   ../Tools/VSCode/src/vscode_resources.scala
 )
diff -r 812c35fbffa8 -r 64dfee6bd243 src/Tools/VSCode/README.md
--- a/src/Tools/VSCode/README.md	Tue Mar 07 10:52:04 2017 +0100
+++ b/src/Tools/VSCode/README.md	Tue Mar 07 13:55:49 2017 +0100
@@ -25,13 +25,9 @@
 
 ## Build ##
 
-* shell> `cd src/Tools/VSCode/extension`
-
-* shell> `isabelle vscode_grammar`
+* shell> `isabelle build_vscode`
 
-* shell> `isabelle vscode_symbols`
-
-* shell> `vsce package`
+* Extensions / ... / Install from VSIX: src/Tools/VSCode/extension/isabelle-X.Y.Z.vsix
 
 
 ## Relevant links ##
diff -r 812c35fbffa8 -r 64dfee6bd243 src/Tools/VSCode/extension/README.md
--- a/src/Tools/VSCode/extension/README.md	Tue Mar 07 10:52:04 2017 +0100
+++ b/src/Tools/VSCode/extension/README.md	Tue Mar 07 13:55:49 2017 +0100
@@ -28,5 +28,5 @@
 Symbols Mode. It needs to be configured manually as follows:
 
 $ISABELLE_HOME/src/Tools/VSCode/extension/isabelle-symbols.json contains a
-configuration (generated via `isabelle vscode_symbols`). Its content needs to
+configuration (generated via `isabelle build_vscode`). Its content needs to
 be copied carefully into the regular VSCode User Preferences.
diff -r 812c35fbffa8 -r 64dfee6bd243 src/Tools/VSCode/src/build_vscode.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/build_vscode.scala	Tue Mar 07 13:55:49 2017 +0100
@@ -0,0 +1,103 @@
+/*  Title:      Pure/Admin/build_vscode.scala
+    Author:     Makarius
+
+Build VSCode configuration and extension module for Isabelle.
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+
+object Build_VSCode
+{
+  val extension_dir = Path.explode("~~/src/Tools/VSCode/extension")
+
+
+  /* Prettify Symbols Mode */
+
+  def prettify_config: String =
+    """{
+  "prettifySymbolsMode.substitutions": [
+      {
+        "language": "isabelle",
+        "revealOn": "none",
+        "adjustCursorMovement": true,
+        "substitutions": [""" +
+          (for ((s, c) <- Symbol.codes)
+           yield
+            JSON.Format(
+              Map("ugly" -> Library.escape_regex(s),
+                "pretty" -> Library.escape_regex(Codepoint.string(c)))))
+            .mkString("\n          ", ",\n          ", "") +
+        """]
+      }
+    ]
+}"""
+
+  def build_symbols(progress: Progress = No_Progress)
+  {
+    val output_path = extension_dir + Path.explode("isabelle-symbols.json")
+    progress.echo(output_path.implode)
+    File.write_backup(output_path, prettify_config)
+  }
+
+
+  /* grammar */
+
+  def build_grammar(options: Options, progress: Progress = No_Progress)
+  {
+    val logic = Grammar.default_logic
+    val keywords = Build.outer_syntax(options, Nil, logic).keywords
+
+    val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
+    progress.echo(output_path.implode)
+    File.write_backup(output_path, Grammar.generate(keywords))
+  }
+
+
+  /* extension */
+
+  def build_extension(progress: Progress = No_Progress, publish: Boolean = false)
+  {
+    val output_path = extension_dir + Path.explode("out")
+    progress.echo(output_path.implode)
+
+    val cmd = "vsce " + (if (publish) "publish" else "package")
+    progress.bash(cmd, cwd = extension_dir.file, echo = true).check
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("build_vscode", "build Isabelle/VSCode extension module", args =>
+    {
+      var publish = false
+
+      val getopts = Getopts("""
+Usage: isabelle build_vscode
+
+  Options are:
+    -P           publish the package
+
+Build Isabelle/VSCode extension module in directory
+""" + extension_dir.expand + """
+
+This requires npm and the vsce build and publishing tool, see also
+https://code.visualstudio.com/docs/tools/vscecli
+""",
+        "P" -> (_ => publish = true))
+
+      val more_args = getopts(args)
+      if (more_args.nonEmpty) getopts.usage()
+
+      val options = Options.init()
+      val progress = new Console_Progress()
+
+      build_symbols(progress)
+      build_grammar(options, progress)
+      build_extension(progress, publish = publish)
+    }, admin = true)
+}
diff -r 812c35fbffa8 -r 64dfee6bd243 src/Tools/VSCode/src/grammar.scala
--- a/src/Tools/VSCode/src/grammar.scala	Tue Mar 07 10:52:04 2017 +0100
+++ b/src/Tools/VSCode/src/grammar.scala	Tue Mar 07 13:55:49 2017 +0100
@@ -16,9 +16,9 @@
 {
   /* generate grammar */
 
-  private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+  lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
 
-  private def default_output(logic: String = ""): String =
+  def default_output(logic: String = ""): String =
     if (logic == "" || logic == default_logic) "isabelle-grammar.json"
     else "isabelle-" + logic + "-grammar.json"
 
diff -r 812c35fbffa8 -r 64dfee6bd243 src/Tools/VSCode/src/symbols.scala
--- a/src/Tools/VSCode/src/symbols.scala	Tue Mar 07 10:52:04 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-/*  Title:      Tools/VSCode/src/symbols.scala
-    Author:     Makarius
-
-Generate configuration for VSCode editor extension Prettify Symbols Mode.
-*/
-
-package isabelle.vscode
-
-
-import isabelle._
-
-
-object Symbols
-{
-  /* generate configuration */
-
-  def prettify_config: String =
-    """{
-  "prettifySymbolsMode.substitutions": [
-      {
-        "language": "isabelle",
-        "revealOn": "none",
-        "adjustCursorMovement": true,
-        "substitutions": [""" +
-          (for ((s, c) <- Symbol.codes)
-           yield
-            JSON.Format(
-              Map("ugly" -> Library.escape_regex(s),
-                "pretty" -> Library.escape_regex(Codepoint.string(c)))))
-            .mkString("\n          ", ",\n          ", "") +
-        """]
-      }
-    ]
-}"""
-
-
-  /* Isabelle tool wrapper */
-
-  val isabelle_tool = Isabelle_Tool("vscode_symbols",
-    "generate configuration for VSCode Prettify Symbols Mode", args =>
-  {
-    val getopts = Getopts("""
-Usage: isabelle vscode_symbols
-
-  Generate configuration for VSCode editor extension Prettify Symbols Mode.
-""")
-
-    val more_args = getopts(args)
-    if (more_args.nonEmpty) getopts.usage()
-
-    val output_path = Path.explode("isabelle-symbols.json")
-    Output.writeln(output_path.implode)
-    File.write_backup(output_path, prettify_config)
-  })
-}