# HG changeset patch
# User wenzelm
# Date 1606596984 -3600
# Node ID 3cc73d00553c40c786242a706c6588458838f23d
# Parent  d9a54c4c9da9d118335a611c50fb28e106a4f32a
added document antiquotation @{tool};
formal check of isabelle tools via Isabelle/Scala;

diff -r d9a54c4c9da9 -r 3cc73d00553c NEWS
--- a/NEWS	Sat Nov 28 20:18:29 2020 +0100
+++ b/NEWS	Sat Nov 28 21:56:24 2020 +0100
@@ -45,6 +45,10 @@
 * Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
 document output is always PDF.
 
+* Antiquotation @{tool} refers to Isabelle command-line tools, with
+completion and formal reference to the source (external script or
+internal Scala function).
+
 * Antiquotation @{bash_function} refers to GNU bash functions that are
 checked within the Isabelle settings environment.
 
diff -r d9a54c4c9da9 -r 3cc73d00553c etc/symbols
--- a/etc/symbols	Sat Nov 28 20:18:29 2020 +0100
+++ b/etc/symbols	Sat Nov 28 21:56:24 2020 +0100
@@ -432,6 +432,7 @@
 \<^term>                argument: cartouche
 \<^theory>              argument: cartouche
 \<^theory_context>      argument: cartouche
+\<^tool>                argument: cartouche
 \<^typ>                 argument: cartouche
 \<^type_abbrev>         argument: cartouche
 \<^type_name>           argument: cartouche
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Doc/System/Base.thy
--- a/src/Doc/System/Base.thy	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Doc/System/Base.thy	Sat Nov 28 21:56:24 2020 +0100
@@ -3,7 +3,7 @@
 theory Base
 imports Pure
 begin
-
+                       
 ML_file \<open>../antiquote_setup.ML\<close>
 
 end
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Doc/antiquote_setup.ML	Sat Nov 28 21:56:24 2020 +0100
@@ -201,7 +201,7 @@
     entity_antiqs check_system_option "isasystem" \<^binding>\<open>system_option\<close> #>
     entity_antiqs no_check "" \<^binding>\<open>inference\<close> #>
     entity_antiqs no_check "isasystem" \<^binding>\<open>executable\<close> #>
-    entity_antiqs no_check "isatool" \<^binding>\<open>tool\<close> #>
+    entity_antiqs Isabelle_Tool.check "isatool" \<^binding>\<open>tool\<close> #>
     entity_antiqs ML_Context.check_antiquotation "" \<^binding>\<open>ML_antiquotation\<close> #>
     entity_antiqs (K JEdit.check_action) "isasystem" \<^binding>\<open>action\<close>);
 
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_csdp.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -171,7 +171,7 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("build_csdp", "build prover component from official download",
+    Isabelle_Tool("build_csdp", "build prover component from official download", Scala_Project.here,
     args =>
     {
       var target_dir = Path.current
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/build_cygwin.scala
--- a/src/Pure/Admin/build_cygwin.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_cygwin.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -61,7 +61,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("build_cygwin", "produce pre-canned Cygwin distribution for Isabelle", args =>
+    Isabelle_Tool("build_cygwin", "produce pre-canned Cygwin distribution for Isabelle",
+      Scala_Project.here, args =>
     {
       var mirror = default_mirror
       var more_packages: List[String] = Nil
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_doc.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -72,7 +72,7 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("build_doc", "build Isabelle documentation", args =>
+    Isabelle_Tool("build_doc", "build Isabelle documentation", Scala_Project.here, args =>
     {
       var all_docs = false
       var max_jobs = 1
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/build_e.scala
--- a/src/Pure/Admin/build_e.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_e.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -108,7 +108,7 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("build_e", "build prover component from source distribution",
+    Isabelle_Tool("build_e", "build prover component from source distribution", Scala_Project.here,
     args =>
     {
       var target_dir = Path.current
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_fonts.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -335,7 +335,7 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("build_fonts", "construct Isabelle fonts", args =>
+    Isabelle_Tool("build_fonts", "construct Isabelle fonts", Scala_Project.here, args =>
     {
       var source_dirs: List[Path] = Nil
 
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_jdk.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -214,7 +214,7 @@
 
   val isabelle_tool =
     Isabelle_Tool("build_jdk", "build Isabelle jdk component from original archives",
-    args =>
+      Scala_Project.here, args =>
     {
       var target_dir = Path.current
 
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -204,7 +204,7 @@
   /** Isabelle tool wrappers **/
 
   val isabelle_tool1 =
-    Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
+    Isabelle_Tool("build_polyml", "build Poly/ML from sources", Scala_Project.here, args =>
     {
       var mingw = MinGW.none
       var arch_64 = Isabelle_Platform.self.is_arm
@@ -242,7 +242,8 @@
     })
 
   val isabelle_tool2 =
-    Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", args =>
+    Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component",
+      Scala_Project.here, args =>
     {
       var sha1_root: Option[Path] = None
 
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/build_spass.scala
--- a/src/Pure/Admin/build_spass.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_spass.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -147,7 +147,7 @@
 
   val isabelle_tool =
     Isabelle_Tool("build_spass", "build prover component from source distribution",
-    args =>
+      Scala_Project.here, args =>
     {
       var target_dir = Path.current
       var download_url = default_download_url
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/build_sqlite.scala
--- a/src/Pure/Admin/build_sqlite.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_sqlite.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -84,7 +84,7 @@
 
   val isabelle_tool =
     Isabelle_Tool("build_sqlite", "build Isabelle sqlite-jdbc component from official download",
-    args =>
+      Scala_Project.here, args =>
     {
       var target_dir = Path.current
 
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -573,7 +573,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("build_status", "present recent build status information from database", args =>
+    Isabelle_Tool("build_status", "present recent build status information from database",
+      Scala_Project.here, args =>
     {
       var target_dir = default_target_dir
       var ml_statistics = false
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/build_verit.scala
--- a/src/Pure/Admin/build_verit.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_verit.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -124,7 +124,7 @@
 
   val isabelle_tool =
     Isabelle_Tool("build_verit", "build prover component from official download",
-    args =>
+      Scala_Project.here, args =>
     {
       var target_dir = Path.current
       var mingw = MinGW.none
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/build_zipperposition.scala
--- a/src/Pure/Admin/build_zipperposition.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_zipperposition.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -90,7 +90,7 @@
 
   val isabelle_tool =
     Isabelle_Tool("build_zipperposition", "build prover component from OPAM repository",
-    args =>
+      Scala_Project.here, args =>
     {
       var target_dir = Path.current
       var version = default_version
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/check_sources.scala
--- a/src/Pure/Admin/check_sources.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/check_sources.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -63,7 +63,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", args =>
+    Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources",
+      Scala_Project.here, args =>
     {
       val getopts = Getopts("""
 Usage: isabelle check_sources [ROOT_DIRS...]
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/components.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -262,7 +262,8 @@
     List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir")
 
   val isabelle_tool =
-    Isabelle_Tool("build_components", "build and publish Isabelle components", args =>
+    Isabelle_Tool("build_components", "build and publish Isabelle components",
+      Scala_Project.here, args =>
     {
       var publish = false
       var update_components_sha1 = false
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/General/mercurial.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -298,7 +298,8 @@
   }
 
   val isabelle_tool =
-    Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository", args =>
+    Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository",
+      Scala_Project.here, args =>
     {
       var remote_name = ""
       var path_name = default_path_name
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/ML/ml_process.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -141,7 +141,8 @@
 
   /* Isabelle tool wrapper */
 
-  val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
+  val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)",
+    Scala_Project.here, args =>
   {
     var dirs: List[Path] = Nil
     var eval_args: List[String] = Nil
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Nov 28 21:56:24 2020 +0100
@@ -68,6 +68,7 @@
   val export_pathN: string val export_path: string -> T
   val urlN: string val url: string -> T
   val docN: string val doc: string -> T
+  val toolN: string val tool: string -> T
   val markupN: string
   val consistentN: string
   val unbreakableN: string
@@ -403,6 +404,7 @@
 val (export_pathN, export_path) = markup_string "export_path" nameN;
 val (urlN, url) = markup_string "url" nameN;
 val (docN, doc) = markup_string "doc" nameN;
+val (toolN, tool) = markup_string "tool" nameN;
 
 
 (* pretty printing *)
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/ROOT.ML	Sat Nov 28 21:56:24 2020 +0100
@@ -326,6 +326,7 @@
 ML_file "System/isabelle_process.ML";
 ML_file "System/scala.ML";
 ML_file "System/scala_compiler.ML";
+ML_file "System/isabelle_tool.ML";
 ML_file "Thy/bibtex.ML";
 ML_file "PIDE/protocol.ML";
 ML_file "General/output_primitives_virtual.ML";
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/System/isabelle_tool.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_tool.ML	Sat Nov 28 21:56:24 2020 +0100
@@ -0,0 +1,44 @@
+(*  Title:      Pure/System/isabelle_tool.ML
+    Author:     Makarius
+
+Support for Isabelle system tools.
+*)
+
+signature ISABELLE_TOOL =
+sig
+  val isabelle_tools: unit -> (string * Position.T) list
+  val check: Proof.context -> string * Position.T -> string
+end;
+
+structure Isabelle_Tool: ISABELLE_TOOL =
+struct
+
+(* list tools *)
+
+fun symbolic_file (a, b) =
+  if a = Markup.fileN
+  then (a, Path.explode b |> Path.implode_symbolic)
+  else (a, b);
+
+fun isabelle_tools () =
+  \<^scala>\<open>isabelle_tools\<close> ""
+  |> YXML.parse_body
+  |> let open XML.Decode in list (pair string properties) end
+  |> map (apsnd (map symbolic_file #> Position.of_properties));
+
+
+(* check *)
+
+fun check ctxt arg =
+  Completion.check_item Markup.toolN
+    (fn (name, pos) =>
+      Markup.entity Markup.toolN name
+      |> Markup.properties (Position.def_properties_of pos))
+    (isabelle_tools ()) ctxt arg;
+
+val _ =
+  Theory.setup
+   (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>tool\<close>
+      (Scan.lift Parse.embedded_position) check);
+
+end;
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -9,7 +9,7 @@
 
 import java.net.URLClassLoader
 import scala.reflect.runtime.universe
-import scala.tools.reflect.{ToolBox,ToolBoxError}
+import scala.tools.reflect.{ToolBox, ToolBoxError}
 
 
 object Isabelle_Tool
@@ -66,21 +66,6 @@
     catch { case _: SecurityException => false }
   }
 
-  private def list_external(): List[(String, String)] =
-  {
-    val Description = """.*\bDESCRIPTION: *(.*)""".r
-    for {
-      dir <- dirs() if dir.is_dir
-      file_name <- File.read_dir(dir) if is_external(dir, file_name)
-    } yield {
-      val source = File.read(dir + Path.explode(file_name))
-      val name = Library.perhaps_unsuffix(".scala", file_name)
-      val description =
-        split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
-      (name, description)
-    }
-  }
-
   private def find_external(name: String): Option[List[String] => Unit] =
     dirs().collectFirst({
       case dir if is_external(dir, name + ".scala") =>
@@ -100,10 +85,6 @@
   private lazy val internal_tools: List[Isabelle_Tool] =
     Isabelle_System.make_services(classOf[Isabelle_Scala_Tools]).flatMap(_.tools)
 
-  private def list_internal(): List[(String, String)] =
-    for (tool <- internal_tools.toList)
-      yield (tool.name, tool.description)
-
   private def find_internal(name: String): Option[List[String] => Unit] =
     internal_tools.collectFirst({
       case tool if tool.name == name =>
@@ -111,6 +92,58 @@
       })
 
 
+  /* list tools */
+
+  abstract class Entry
+  {
+    def name: String
+    def position: Properties.T
+    def description: String
+    def print: String =
+      description match {
+        case "" => name
+        case descr => name + " - " + descr
+      }
+  }
+
+  sealed case class External(name: String, path: Path) extends Entry
+  {
+    def position: Properties.T = Position.File(path.absolute.implode)
+    def description: String =
+    {
+      val Pattern = """.*\bDESCRIPTION: *(.*)""".r
+      split_lines(File.read(path)).collectFirst({ case Pattern(s) => s }) getOrElse ""
+    }
+  }
+
+  def external_tools(): List[External] =
+  {
+    for {
+      dir <- dirs() if dir.is_dir
+      file_name <- File.read_dir(dir) if is_external(dir, file_name)
+    } yield {
+      val path = dir + Path.explode(file_name)
+      val name = Library.perhaps_unsuffix(".scala", file_name)
+      External(name, path)
+    }
+  }
+
+  def isabelle_tools(): List[Entry] =
+    (external_tools() ::: internal_tools).sortBy(_.name)
+
+  object Isabelle_Tools extends Scala.Fun("isabelle_tools")
+  {
+    val here = Scala_Project.here
+    def apply(arg: String): String =
+      if (arg.nonEmpty) error("Bad argument: " + quote(arg))
+      else {
+        val result = isabelle_tools().map(entry => (entry.name, entry.position))
+        val body = { import XML.Encode._; list(pair(string, properties))(result) }
+        YXML.string_of_body(body)
+      }
+  }
+
+
   /* command line entry point */
 
   def main(args: Array[String])
@@ -118,9 +151,7 @@
     Command_Line.tool {
       args.toList match {
         case Nil | List("-?") =>
-          val tool_descriptions =
-            (list_external() ::: list_internal()).sortBy(_._1).
-              map({ case (a, "") => a case (a, b) => a + " - " + b })
+          val tool_descriptions = isabelle_tools().map(_.print)
           Getopts("""
 Usage: isabelle TOOL [ARGS ...]
 
@@ -137,7 +168,14 @@
   }
 }
 
-sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
+sealed case class Isabelle_Tool(
+  name: String,
+  description: String,
+  here: Scala_Project.Here,
+  body: List[String] => Unit) extends Isabelle_Tool.Entry
+{
+  def position: Position.T = here.position
+}
 
 class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service
 
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/System/options.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -148,7 +148,8 @@
 
   /* Isabelle tool wrapper */
 
-  val isabelle_tool = Isabelle_Tool("options", "print Isabelle system options", args =>
+  val isabelle_tool = Isabelle_Tool("options", "print Isabelle system options",
+    Scala_Project.here, args =>
   {
     var build_options = false
     var get_option = ""
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/System/scala.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -243,4 +243,5 @@
   Scala.Sleep,
   Scala.Toplevel,
   Doc.Doc_Names,
-  Bibtex.Check_Database)
+  Bibtex.Check_Database,
+  Isabelle_Tool.Isabelle_Tools)
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Thy/export.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -372,7 +372,8 @@
 
   val default_export_dir: Path = Path.explode("export")
 
-  val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args =>
+  val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports",
+    Scala_Project.here, args =>
   {
     /* arguments */
 
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -612,7 +612,7 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("document", "prepare session theory document", args =>
+    Isabelle_Tool("document", "prepare session theory document", Scala_Project.here, args =>
     {
       var output_sources: Option[Path] = None
       var output_pdf: Option[Path] = None
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -1048,7 +1048,8 @@
 
   /* Isabelle tool wrapper */
 
-  val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions", args =>
+  val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions",
+    Scala_Project.here, args =>
   {
     var base_sessions: List[String] = Nil
     var select_dirs: List[Path] = Nil
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/build.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -526,7 +526,8 @@
 
   /* Isabelle tool wrapper */
 
-  val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
+  val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions",
+    Scala_Project.here, args =>
   {
     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
 
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/build_docker.scala
--- a/src/Pure/Tools/build_docker.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/build_docker.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -100,7 +100,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("build_docker", "build Isabelle docker image", args =>
+    Isabelle_Tool("build_docker", "build Isabelle docker image",
+      Scala_Project.here, args =>
     {
       var base = default_base
       var entrypoint = false
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/doc.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -100,7 +100,8 @@
 
   /* Isabelle tool wrapper */
 
-  val isabelle_tool = Isabelle_Tool("doc", "view Isabelle documentation", args =>
+  val isabelle_tool = Isabelle_Tool("doc", "view Isabelle documentation",
+    Scala_Project.here, args =>
   {
     val getopts = Getopts("""
 Usage: isabelle doc [DOC ...]
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/dump.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -420,7 +420,7 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
+    Isabelle_Tool("dump", "dump cumulative PIDE session database", Scala_Project.here, args =>
     {
       var aspects: List[Aspect] = known_aspects
       var base_sessions: List[String] = Nil
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/mkroot.scala
--- a/src/Pure/Tools/mkroot.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/mkroot.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -176,7 +176,8 @@
 
   /** Isabelle tool wrapper **/
 
-  val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory", args =>
+  val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory",
+    Scala_Project.here, args =>
   {
     var author = ""
     var init_repos = false
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/phabricator.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -146,7 +146,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool1 =
-    Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory", args =>
+    Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory",
+      Scala_Project.here, args =>
     {
       var list = false
       var name = default_name
@@ -535,7 +536,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool2 =
-    Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", args =>
+    Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux",
+      Scala_Project.here, args =>
     {
       var mercurial_source = ""
       var repo = ""
@@ -642,8 +644,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool3 =
-    Isabelle_Tool("phabricator_setup_mail",
-      "setup mail for one Phabricator installation", args =>
+    Isabelle_Tool("phabricator_setup_mail", "setup mail for one Phabricator installation",
+      Scala_Project.here, args =>
     {
       var test_user = ""
       var name = default_name
@@ -805,8 +807,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool4 =
-    Isabelle_Tool("phabricator_setup_ssh",
-      "setup ssh service for all Phabricator installations", args =>
+    Isabelle_Tool("phabricator_setup_ssh", "setup ssh service for all Phabricator installations",
+      Scala_Project.here, args =>
     {
       var server_port = default_server_port
       var system_port = default_system_port
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/profiling_report.scala
--- a/src/Pure/Tools/profiling_report.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/profiling_report.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -30,7 +30,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files", args =>
+    Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files",
+      Scala_Project.here, args =>
     {
       val getopts =
         Getopts("""
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/scala_project.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -161,7 +161,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("scala_project", "setup Gradle project for Isabelle/Scala/jEdit", args =>
+    Isabelle_Tool("scala_project", "setup Gradle project for Isabelle/Scala/jEdit",
+      Scala_Project.here, args =>
     {
       var symlinks = false
 
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/server.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -418,7 +418,7 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("server", "manage resident Isabelle servers", args =>
+    Isabelle_Tool("server", "manage resident Isabelle servers", Scala_Project.here, args =>
     {
       var console = false
       var log_file: Option[Path] = None
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/update.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -63,7 +63,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("update", "update theory sources based on PIDE markup", args =>
+    Isabelle_Tool("update", "update theory sources based on PIDE markup", Scala_Project.here,
+      args =>
     {
       var base_sessions: List[String] = Nil
       var select_dirs: List[Path] = Nil
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/update_cartouches.scala
--- a/src/Pure/Tools/update_cartouches.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/update_cartouches.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -84,7 +84,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches", args =>
+    Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches",
+      Scala_Project.here, args =>
     {
       var replace_text = false
 
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/update_comments.scala
--- a/src/Pure/Tools/update_comments.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/update_comments.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -47,7 +47,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("update_comments", "update formal comments in outer syntax", args =>
+    Isabelle_Tool("update_comments", "update formal comments in outer syntax",
+      Scala_Project.here, args =>
     {
       val getopts = Getopts("""
 Usage: isabelle update_comments [FILES|DIRS...]
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/update_header.scala
--- a/src/Pure/Tools/update_header.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/update_header.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -29,7 +29,8 @@
     Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph")
 
   val isabelle_tool =
-    Isabelle_Tool("update_header", "replace obsolete theory header command", args =>
+    Isabelle_Tool("update_header", "replace obsolete theory header command",
+      Scala_Project.here, args =>
     {
       var section = "section"
 
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/update_then.scala
--- a/src/Pure/Tools/update_then.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/update_then.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -31,7 +31,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("update_then", "expand old Isar command conflations 'hence' and 'thus'", args =>
+    Isabelle_Tool("update_then", "expand old Isar command conflations 'hence' and 'thus'",
+      Scala_Project.here, args =>
     {
       val getopts = Getopts("""
 Usage: isabelle update_then [FILES|DIRS...]
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/Tools/update_theorems.scala
--- a/src/Pure/Tools/update_theorems.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/update_theorems.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -31,7 +31,8 @@
 
   /* Isabelle tool wrapper */
 
-  val isabelle_tool = Isabelle_Tool("update_theorems", "update toplevel theorem keywords", args =>
+  val isabelle_tool = Isabelle_Tool("update_theorems", "update toplevel theorem keywords",
+    Scala_Project.here, args =>
   {
     val getopts = Getopts("""
 Usage: isabelle update_theorems [FILES|DIRS...]
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Tools/VSCode/src/build_vscode.scala
--- a/src/Tools/VSCode/src/build_vscode.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Tools/VSCode/src/build_vscode.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -44,7 +44,8 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("build_vscode", "build Isabelle/VSCode extension module", args =>
+    Isabelle_Tool("build_vscode", "build Isabelle/VSCode extension module",
+      Scala_Project.here, args =>
     {
       var publish = false
 
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Tools/VSCode/src/grammar.scala
--- a/src/Tools/VSCode/src/grammar.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Tools/VSCode/src/grammar.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -134,7 +134,7 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("vscode_grammar",
-    "generate static TextMate grammar for VSCode editor", args =>
+    "generate static TextMate grammar for VSCode editor", Scala_Project.here, args =>
   {
     var dirs: List[Path] = Nil
     var logic = default_logic
diff -r d9a54c4c9da9 -r 3cc73d00553c src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Sat Nov 28 21:56:24 2020 +0100
@@ -28,20 +28,21 @@
 
   private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
 
-  val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args =>
-  {
-    try {
-      var logic_ancestor: Option[String] = None
-      var log_file: Option[Path] = None
-      var logic_requirements = false
-      var dirs: List[Path] = Nil
-      var include_sessions: List[String] = Nil
-      var logic = default_logic
-      var modes: List[String] = Nil
-      var options = Options.init()
-      var verbose = false
+  val isabelle_tool =
+    Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", Scala_Project.here, args =>
+    {
+      try {
+        var logic_ancestor: Option[String] = None
+        var log_file: Option[Path] = None
+        var logic_requirements = false
+        var dirs: List[Path] = Nil
+        var include_sessions: List[String] = Nil
+        var logic = default_logic
+        var modes: List[String] = Nil
+        var options = Options.init()
+        var verbose = false
 
-      val getopts = Getopts("""
+        val getopts = Getopts("""
 Usage: isabelle vscode_server [OPTIONS]
 
   Options are:
@@ -57,41 +58,41 @@
 
   Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
 """,
-        "A:" -> (arg => logic_ancestor = Some(arg)),
-        "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
-        "R:" -> (arg => { logic = arg; logic_requirements = true }),
-        "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
-        "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
-        "l:" -> (arg => logic = arg),
-        "m:" -> (arg => modes = arg :: modes),
-        "o:" -> (arg => options = options + arg),
-        "v" -> (_ => verbose = true))
+          "A:" -> (arg => logic_ancestor = Some(arg)),
+          "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
+          "R:" -> (arg => { logic = arg; logic_requirements = true }),
+          "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
+          "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
+          "l:" -> (arg => logic = arg),
+          "m:" -> (arg => modes = arg :: modes),
+          "o:" -> (arg => options = options + arg),
+          "v" -> (_ => verbose = true))
 
-      val more_args = getopts(args)
-      if (more_args.nonEmpty) getopts.usage()
+        val more_args = getopts(args)
+        if (more_args.nonEmpty) getopts.usage()
 
-      val log = Logger.make(log_file)
-      val channel = new Channel(System.in, System.out, log, verbose)
-      val server =
-        new Language_Server(channel, options, session_name = logic, session_dirs = dirs,
-          include_sessions = include_sessions, session_ancestor = logic_ancestor,
-          session_requirements = logic_requirements, modes = modes, log = log)
+        val log = Logger.make(log_file)
+        val channel = new Channel(System.in, System.out, log, verbose)
+        val server =
+          new Language_Server(channel, options, session_name = logic, session_dirs = dirs,
+            include_sessions = include_sessions, session_ancestor = logic_ancestor,
+            session_requirements = logic_requirements, modes = modes, log = log)
 
-      // prevent spurious garbage on the main protocol channel
-      val orig_out = System.out
-      try {
-        System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))
-        server.start()
+        // prevent spurious garbage on the main protocol channel
+        val orig_out = System.out
+        try {
+          System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))
+          server.start()
+        }
+        finally { System.setOut(orig_out) }
       }
-      finally { System.setOut(orig_out) }
-    }
-    catch {
-      case exn: Throwable =>
-        val channel = new Channel(System.in, System.out, No_Logger)
-        channel.error_message(Exn.message(exn))
-        throw(exn)
-    }
-  })
+      catch {
+        case exn: Throwable =>
+          val channel = new Channel(System.in, System.out, No_Logger)
+          channel.error_message(Exn.message(exn))
+          throw(exn)
+      }
+    })
 }
 
 class Language_Server(