another isabelle_scala_service;
authorwenzelm
Wed, 08 Apr 2020 14:25:28 +0200
changeset 71736 a2afc7ed2c68
parent 71735 9644811b5b0a
child 71737 7ff701556063
another isabelle_scala_service;
NEWS
etc/settings
lib/scripts/getfunctions
src/Pure/System/isabelle_tool.scala
--- a/NEWS	Wed Apr 08 14:09:32 2020 +0200
+++ b/NEWS	Wed Apr 08 14:25:28 2020 +0200
@@ -18,8 +18,9 @@
 
 * General support for Isabelle/Scala system services, configured via the
 shell function "isabelle_scala_service" in etc/settings (e.g. of an
-Isabelle component); e.g. see isabelle.Bibtex.File_Format. This
-supersedes former "isabelle_file_format": minor INCOMPATIBILITY.
+Isabelle component). For example, see isabelle.Bibtex.File_Format. This
+supersedes former "isabelle_scala_tools" and "isabelle_file_format":
+minor INCOMPATIBILITY.
 
 
 
--- a/etc/settings	Wed Apr 08 14:09:32 2020 +0200
+++ b/etc/settings	Wed Apr 08 14:25:28 2020 +0200
@@ -20,8 +20,8 @@
 
 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
 
-isabelle_scala_tools 'isabelle.Tools'
-[ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_tools 'isabelle.Admin_Tools'
+isabelle_scala_service 'isabelle.Tools'
+[ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools'
 
 isabelle_scala_service 'isabelle.Bibtex$File_Format'
 
--- a/lib/scripts/getfunctions	Wed Apr 08 14:09:32 2020 +0200
+++ b/lib/scripts/getfunctions	Wed Apr 08 14:25:28 2020 +0200
@@ -113,22 +113,6 @@
 }
 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
-
 #Isabelle fonts
 function isabelle_fonts ()
 {
--- a/src/Pure/System/isabelle_tool.scala	Wed Apr 08 14:09:32 2020 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Wed Apr 08 14:25:28 2020 +0200
@@ -98,7 +98,7 @@
   /* internal tools */
 
   private lazy val internal_tools: List[Isabelle_Tool] =
-    Isabelle_System.init_classes[Isabelle_Scala_Tools]("ISABELLE_SCALA_TOOLS")
+    Isabelle_System.services.collect { case c: Isabelle_Scala_Tools => c }
       .flatMap(_.tools.toList)
 
   private def list_internal(): List[(String, String)] =
@@ -140,7 +140,7 @@
 
 sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
 
-class Isabelle_Scala_Tools(val tools: Isabelle_Tool*)
+class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service
 
 class Tools extends Isabelle_Scala_Tools(
   Build.isabelle_tool,