# HG changeset patch
# User wenzelm
# Date 1541855282 -3600
# Node ID 258bef08b31e81189c8d1a56f0938d3f8dfb336d
# Parent  3d954183b707305984051f0763ac82c110b63d50
support for user-defined Isabelle/Scala command-line tools;
misc tuning and clarification;

diff -r 3d954183b707 -r 258bef08b31e NEWS
--- a/NEWS	Sat Nov 10 07:57:20 2018 +0000
+++ b/NEWS	Sat Nov 10 14:08:02 2018 +0100
@@ -26,9 +26,9 @@
 OpenJDK 11.
 
 * Support for user-defined file-formats via class isabelle.File_Format
-in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format). It is
-configured via the shell function "isabelle_file_format" in
-etc/settings, e.g. of an Isabelle component.
+in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via
+the shell function "isabelle_file_format" in etc/settings (e.g. of an
+Isabelle component).
 
 
 *** Isar ***
@@ -117,6 +117,11 @@
 
 *** System ***
 
+* Support for Isabelle command-line tools defined in Isabelle/Scala.
+Instances of class Isabelle_Scala_Tools may be configured via the shell
+function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
+component).
+
 * Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
 source modules for Isabelle tools implemented in Haskell, notably for
 Isabelle/PIDE.
diff -r 3d954183b707 -r 258bef08b31e etc/settings
--- a/etc/settings	Sat Nov 10 07:57:20 2018 +0000
+++ b/etc/settings	Sat Nov 10 14:08:02 2018 +0100
@@ -20,6 +20,9 @@
 
 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
 
+isabelle_scala_tools 'isabelle.Regular_Tools'
+[ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_tools 'isabelle.Admin_Tools'
+
 isabelle_file_format 'isabelle.Bibtex$File_Format'
 
 #paranoia settings -- avoid intrusion of alien options
diff -r 3d954183b707 -r 258bef08b31e lib/scripts/getfunctions
--- a/lib/scripts/getfunctions	Sat Nov 10 07:57:20 2018 +0000
+++ b/lib/scripts/getfunctions	Sat Nov 10 14:08:02 2018 +0100
@@ -109,19 +109,35 @@
 }
 export -f classpath
 
+#Isabelle/Scala tools
+function isabelle_scala_tools ()
+{
+  local X=""
+  for X in "$@"
+  do
+    if [ -z "$ISABELLE_SCALA_TOOLS" ]; then
+      ISABELLE_SCALA_TOOLS="$X"
+    else
+      ISABELLE_SCALA_TOOLS="$ISABELLE_SCALA_TOOLS:$X"
+    fi
+  done
+  export ISABELLE_SCALA_TOOLS
+}
+export -f isabelle_scala_tools
+
 #file formats
 function isabelle_file_format ()
 {
   local X=""
   for X in "$@"
   do
-    if [ -z "$ISABELLE_CLASSES_FILE_FORMAT" ]; then
-      ISABELLE_CLASSES_FILE_FORMAT="$X"
+    if [ -z "$ISABELLE_FILE_FORMATS" ]; then
+      ISABELLE_FILE_FORMATS="$X"
     else
-      ISABELLE_CLASSES_FILE_FORMAT="$ISABELLE_CLASSES_FILE_FORMAT:$X"
+      ISABELLE_FILE_FORMATS="$ISABELLE_FILE_FORMATS:$X"
     fi
   done
-  export ISABELLE_CLASSES_FILE_FORMAT
+  export ISABELLE_FILE_FORMATS
 }
 export -f isabelle_file_format
 
diff -r 3d954183b707 -r 258bef08b31e src/Pure/Admin/build_cygwin.scala
--- a/src/Pure/Admin/build_cygwin.scala	Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/build_cygwin.scala	Sat Nov 10 14:08:02 2018 +0100
@@ -87,5 +87,5 @@
       if (more_args.nonEmpty) getopts.usage()
 
       build_cygwin(new Console_Progress(), mirror = mirror, more_packages = more_packages)
-    }, admin = true)
+    })
 }
diff -r 3d954183b707 -r 258bef08b31e src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/build_doc.scala	Sat Nov 10 14:08:02 2018 +0100
@@ -105,5 +105,5 @@
           build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
         }
       sys.exit(rc)
-    }, admin = true)
+    })
 }
diff -r 3d954183b707 -r 258bef08b31e src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/build_jdk.scala	Sat Nov 10 14:08:02 2018 +0100
@@ -237,5 +237,5 @@
       val progress = new Console_Progress()
 
       build_jdk(archives = archives, progress = progress, target_dir = target_dir)
-    }, admin = true)
+    })
 }
diff -r 3d954183b707 -r 258bef08b31e src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/build_polyml.scala	Sat Nov 10 14:08:02 2018 +0100
@@ -272,7 +272,7 @@
         build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
           arch_64 = arch_64, options = options, msys_root = msys_root)
       }
-    }, admin = true)
+    })
 
   val isabelle_tool2 =
     Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", args =>
@@ -298,5 +298,5 @@
           }
         build_polyml_component(component, sha1_root = sha1_root)
       }
-    }, admin = true)
+    })
 }
diff -r 3d954183b707 -r 258bef08b31e src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/build_status.scala	Sat Nov 10 14:08:02 2018 +0100
@@ -591,6 +591,5 @@
 
       build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose,
         target_dir = target_dir, ml_statistics = ml_statistics, image_size = image_size)
-
-  }, admin = true)
+    })
 }
diff -r 3d954183b707 -r 258bef08b31e src/Pure/Admin/check_sources.scala
--- a/src/Pure/Admin/check_sources.scala	Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/check_sources.scala	Sat Nov 10 14:08:02 2018 +0100
@@ -70,5 +70,5 @@
       if (specs.isEmpty) getopts.usage()
 
       for (root <- specs) check_hg(Path.explode(root))
-    }, admin = true)
+    })
 }
diff -r 3d954183b707 -r 258bef08b31e src/Pure/Admin/remote_dmg.scala
--- a/src/Pure/Admin/remote_dmg.scala	Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/remote_dmg.scala	Sat Nov 10 14:08:02 2018 +0100
@@ -60,5 +60,5 @@
         using(SSH.open_session(options, host = host, user = user, port = port))(
           remote_dmg(_, tar_gz_file, dmg_file, volume_name))
       }
-    }, admin = true)
+    })
 }
diff -r 3d954183b707 -r 258bef08b31e src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/System/isabelle_system.scala	Sat Nov 10 14:08:02 2018 +0100
@@ -347,6 +347,24 @@
     Path.split(getenv_strict("ISABELLE_COMPONENTS"))
 
 
+  /* classes */
+
+  def init_classes[A](variable: String): List[A] =
+  {
+    for (name <- space_explode(':', Isabelle_System.getenv_strict(variable)))
+    yield {
+      def err(msg: String): Nothing =
+        error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
+
+      try { Class.forName(name).asInstanceOf[Class[A]].newInstance() }
+      catch {
+        case _: ClassNotFoundException => err("Class not found")
+        case exn: Throwable => err(Exn.message(exn))
+      }
+    }
+  }
+
+
   /* fonts */
 
   def fonts(html: Boolean = false, get: String => String = getenv_strict(_)): List[Path] =
diff -r 3d954183b707 -r 258bef08b31e src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/System/isabelle_tool.scala	Sat Nov 10 14:08:02 2018 +0100
@@ -97,44 +97,17 @@
 
   /* internal tools */
 
-  private val internal_tools: List[Isabelle_Tool] =
-    List(
-      Build.isabelle_tool,
-      Build_Cygwin.isabelle_tool,
-      Build_Doc.isabelle_tool,
-      Build_Docker.isabelle_tool,
-      Build_JDK.isabelle_tool,
-      Build_PolyML.isabelle_tool1,
-      Build_PolyML.isabelle_tool2,
-      Build_Status.isabelle_tool,
-      Check_Sources.isabelle_tool,
-      Doc.isabelle_tool,
-      Dump.isabelle_tool,
-      Export.isabelle_tool,
-      Imports.isabelle_tool,
-      Mkroot.isabelle_tool,
-      ML_Process.isabelle_tool,
-      Options.isabelle_tool,
-      Present.isabelle_tool,
-      Profiling_Report.isabelle_tool,
-      Remote_DMG.isabelle_tool,
-      Server.isabelle_tool,
-      Update_Cartouches.isabelle_tool,
-      Update_Comments.isabelle_tool,
-      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)
+  private lazy val internal_tools: List[Isabelle_Tool] =
+    Isabelle_System.init_classes[Isabelle_Scala_Tools]("ISABELLE_SCALA_TOOLS")
+      .flatMap(_.tools.toList)
 
   private def list_internal(): List[(String, String)] =
-    for (tool <- internal_tools.toList if tool.accessible)
+    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 && tool.accessible =>
+      case tool if tool.name == name =>
         args => Command_Line.tool0 { tool.body(args) }
       })
 
@@ -165,8 +138,38 @@
   }
 }
 
-sealed case class Isabelle_Tool(
-  name: String, description: String, body: List[String] => Unit, admin: Boolean = false)
-{
-  def accessible: Boolean = !admin || Isabelle_System.admin()
-}
+sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
+
+class Isabelle_Scala_Tools(val tools: Isabelle_Tool*)
+
+class Regular_Tools extends Isabelle_Scala_Tools(
+  Build.isabelle_tool,
+  Build_Docker.isabelle_tool,
+  Doc.isabelle_tool,
+  Dump.isabelle_tool,
+  Export.isabelle_tool,
+  Imports.isabelle_tool,
+  ML_Process.isabelle_tool,
+  Mkroot.isabelle_tool,
+  Options.isabelle_tool,
+  Present.isabelle_tool,
+  Profiling_Report.isabelle_tool,
+  Server.isabelle_tool,
+  Update_Cartouches.isabelle_tool,
+  Update_Comments.isabelle_tool,
+  Update_Header.isabelle_tool,
+  Update_Then.isabelle_tool,
+  Update_Theorems.isabelle_tool,
+  isabelle.vscode.Grammar.isabelle_tool,
+  isabelle.vscode.Server.isabelle_tool)
+
+class Admin_Tools extends Isabelle_Scala_Tools(
+  Build_Cygwin.isabelle_tool,
+  Build_Doc.isabelle_tool,
+  Build_JDK.isabelle_tool,
+  Build_PolyML.isabelle_tool1,
+  Build_PolyML.isabelle_tool2,
+  Build_Status.isabelle_tool,
+  Check_Sources.isabelle_tool,
+  Remote_DMG.isabelle_tool,
+  isabelle.vscode.Build_VSCode.isabelle_tool)
diff -r 3d954183b707 -r 258bef08b31e src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Thy/file_format.scala	Sat Nov 10 14:08:02 2018 +0100
@@ -10,21 +10,7 @@
 object File_Format
 {
   def environment(): Environment =
-  {
-    val file_formats =
-      for (name <- space_explode(':', Isabelle_System.getenv_strict("ISABELLE_CLASSES_FILE_FORMAT")))
-      yield {
-        def err(msg: String): Nothing =
-          error("Bad entry " + quote(name) + " in ISABELLE_CLASSES_FILE_FORMAT\n" + msg)
-
-        try { Class.forName(name).asInstanceOf[Class[File_Format]].newInstance() }
-        catch {
-          case _: ClassNotFoundException => err("Class not found")
-          case exn: Throwable => err(Exn.message(exn))
-        }
-      }
-    new Environment(file_formats)
-  }
+    new Environment(Isabelle_System.init_classes[File_Format]("ISABELLE_FILE_FORMATS"))
 
   final class Environment private [File_Format](file_formats: List[File_Format])
   {
diff -r 3d954183b707 -r 258bef08b31e src/Tools/VSCode/src/build_vscode.scala
--- a/src/Tools/VSCode/src/build_vscode.scala	Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Tools/VSCode/src/build_vscode.scala	Sat Nov 10 14:08:02 2018 +0100
@@ -70,5 +70,5 @@
 
       build_grammar(options, progress)
       build_extension(progress, publish = publish)
-    }, admin = true)
+    })
 }