# HG changeset patch
# User wenzelm
# Date 1586350374 -7200
# Node ID 7ff7015560634f1b5d0f01d3e4754be5e73fd909
# Parent  ada8812f5a9ede7ce0d9248149f1a4ef8a8acb0f# Parent  a2afc7ed2c68113b7cb5796f2e3e1d7de0f88fcd
merged

diff -r ada8812f5a9e -r 7ff701556063 NEWS
--- a/NEWS	Wed Apr 08 14:48:55 2020 +0200
+++ b/NEWS	Wed Apr 08 14:52:54 2020 +0200
@@ -12,8 +12,15 @@
 * The command-line tool "isabelle console" now supports interrupts
 properly (on Linux and macOS).
 
-* The Isabelle/Scala "Progress" interface has changed slightly and
-"No_Progress" discontinued. INCOMPATIBILITY, use "new Progress" instead.
+* The Isabelle/Scala "Progress" interface changed slightly and
+"No_Progress" has been discontinued. INCOMPATIBILITY, use "new Progress"
+instead.
+
+* General support for Isabelle/Scala system services, configured via the
+shell function "isabelle_scala_service" in etc/settings (e.g. of an
+Isabelle component). For example, see isabelle.Bibtex.File_Format. This
+supersedes former "isabelle_scala_tools" and "isabelle_file_format":
+minor INCOMPATIBILITY.
 
 
 
diff -r ada8812f5a9e -r 7ff701556063 etc/settings
--- a/etc/settings	Wed Apr 08 14:48:55 2020 +0200
+++ b/etc/settings	Wed Apr 08 14:52:54 2020 +0200
@@ -20,10 +20,10 @@
 
 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_file_format 'isabelle.Bibtex$File_Format'
+isabelle_scala_service 'isabelle.Bibtex$File_Format'
 
 #paranoia settings -- avoid intrusion of alien options
 unset "_JAVA_OPTIONS"
diff -r ada8812f5a9e -r 7ff701556063 lib/scripts/getfunctions
--- a/lib/scripts/getfunctions	Wed Apr 08 14:48:55 2020 +0200
+++ b/lib/scripts/getfunctions	Wed Apr 08 14:52:54 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 ()
 {
@@ -160,21 +144,21 @@
 }
 export -f isabelle_fonts_hidden
 
-#file formats
-function isabelle_file_format ()
+#Isabelle/Scala services
+function isabelle_scala_service ()
 {
   local X=""
   for X in "$@"
   do
-    if [ -z "$ISABELLE_FILE_FORMATS" ]; then
-      ISABELLE_FILE_FORMATS="$X"
+    if [ -z "$ISABELLE_SCALA_SERVICES" ]; then
+      ISABELLE_SCALA_SERVICES="$X"
     else
-      ISABELLE_FILE_FORMATS="$ISABELLE_FILE_FORMATS:$X"
+      ISABELLE_SCALA_SERVICES="$ISABELLE_SCALA_SERVICES:$X"
     fi
   done
-  export ISABELLE_FILE_FORMATS
+  export ISABELLE_SCALA_SERVICES
 }
-export -f isabelle_file_format
+export -f isabelle_scala_service
 
 #administrative build
 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
diff -r ada8812f5a9e -r 7ff701556063 src/Pure/PIDE/protocol_handlers.scala
--- a/src/Pure/PIDE/protocol_handlers.scala	Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/PIDE/protocol_handlers.scala	Wed Apr 08 14:52:54 2020 +0200
@@ -51,7 +51,10 @@
     def init(name: String): State =
     {
       val new_handler =
-        try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
+        try {
+          Some(Class.forName(name).getDeclaredConstructor().newInstance()
+            .asInstanceOf[Session.Protocol_Handler])
+        }
         catch { case exn: Throwable => bad_handler(exn, name); None }
       new_handler match { case Some(handler) => init(handler) case None => this }
     }
diff -r ada8812f5a9e -r 7ff701556063 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Apr 08 14:52:54 2020 +0200
@@ -23,19 +23,17 @@
 
   /* file formats */
 
-  val file_formats: File_Format.Environment = File_Format.environment()
-
   def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] =
-    file_formats.get(name).flatMap(_.make_theory_name(resources, name))
+    File_Format.registry.get(name).flatMap(_.make_theory_name(resources, name))
 
   def make_theory_content(thy_name: Document.Node.Name): Option[String] =
-    file_formats.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
+    File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
 
   def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
-    file_formats.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
+    File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
 
   def is_hidden(name: Document.Node.Name): Boolean =
-    !name.is_theory || name.theory == Sessions.root_name || file_formats.is_theory(name)
+    !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
 
   def thy_path(path: Path): Path = path.ext("thy")
 
diff -r ada8812f5a9e -r 7ff701556063 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Apr 08 14:52:54 2020 +0200
@@ -354,7 +354,7 @@
   /* file formats */
 
   lazy val file_formats: File_Format.Session =
-    resources.file_formats.start_session(session)
+    File_Format.registry.start_session(session)
 
 
   /* protocol handlers */
diff -r ada8812f5a9e -r 7ff701556063 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Apr 08 14:52:54 2020 +0200
@@ -54,7 +54,7 @@
     _settings.get
   }
 
-  def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized {
+  private def init_settings(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized {
     if (_settings.isEmpty) {
       val isabelle_root1 =
         bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
@@ -127,6 +127,12 @@
     }
   }
 
+  def init()
+  {
+    init_settings()
+    services
+  }
+
 
   /* getenv */
 
@@ -374,7 +380,9 @@
       def err(msg: String): Nothing =
         error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
 
-      try { Class.forName(name).asInstanceOf[Class[A]].newInstance() }
+      try {
+        Class.forName(name).asInstanceOf[Class[A]].getDeclaredConstructor().newInstance()
+      }
       catch {
         case _: ClassNotFoundException => err("Class not found")
         case exn: Throwable => err(Exn.message(exn))
@@ -383,6 +391,13 @@
   }
 
 
+  /*  user-defined services */
+
+  abstract class Service
+
+  lazy val services: List[Service] = init_classes[Service]("ISABELLE_SCALA_SERVICES")
+
+
   /* default logic */
 
   def default_logic(args: String*): String =
diff -r ada8812f5a9e -r 7ff701556063 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Wed Apr 08 14:52:54 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,
diff -r ada8812f5a9e -r 7ff701556063 src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/Thy/file_format.scala	Wed Apr 08 14:52:54 2020 +0200
@@ -12,12 +12,12 @@
   sealed case class Theory_Context(name: Document.Node.Name, content: String)
 
 
-  /* environment */
+  /* registry */
 
-  def environment(): Environment =
-    new Environment(Isabelle_System.init_classes[File_Format]("ISABELLE_FILE_FORMATS"))
+  lazy val registry: Registry =
+    new Registry(Isabelle_System.services.collect { case c: File_Format => c })
 
-  final class Environment private [File_Format](file_formats: List[File_Format])
+  final class Registry private [File_Format](file_formats: List[File_Format])
   {
     override def toString: String = file_formats.mkString("File_Format.Environment(", ",", ")")
 
@@ -53,7 +53,7 @@
   object No_Agent extends Agent
 }
 
-trait File_Format
+trait File_Format extends Isabelle_System.Service
 {
   def format_name: String
   override def toString: String = format_name
diff -r ada8812f5a9e -r 7ff701556063 src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala	Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/Tools/spell_checker.scala	Wed Apr 08 14:52:54 2020 +0200
@@ -141,9 +141,9 @@
         permanent_updates
 
     val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
-    val factory_cons = factory_class.getConstructor()
-    factory_cons.setAccessible(true)
-    val factory = factory_cons.newInstance()
+    val factory_constructor = factory_class.getConstructor()
+    factory_constructor.setAccessible(true)
+    val factory = factory_constructor.newInstance()
 
     val add = Untyped.method(factory_class, "add", classOf[String])
 
diff -r ada8812f5a9e -r 7ff701556063 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Tools/VSCode/src/document_model.scala	Wed Apr 08 14:52:54 2020 +0200
@@ -60,7 +60,7 @@
 
   def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model =
     Document_Model(session, editor, node_name, Content.empty,
-      node_required = session.resources.file_formats.is_theory(node_name))
+      node_required = File_Format.registry.is_theory(node_name))
 }
 
 sealed case class Document_Model(
diff -r ada8812f5a9e -r 7ff701556063 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Apr 08 14:52:54 2020 +0200
@@ -389,7 +389,7 @@
     file.foreach(PIDE.plugin.file_watcher.register_parent(_))
 
     val content = Document_Model.File_Content(text)
-    val node_required1 = node_required || session.resources.file_formats.is_theory(node_name)
+    val node_required1 = node_required || File_Format.registry.is_theory(node_name)
     File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
   }
 }
@@ -454,7 +454,7 @@
 
   def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
     if (pending_edits.nonEmpty ||
-        !session.resources.file_formats.is_theory(node_name) &&
+        !File_Format.registry.is_theory(node_name) &&
           (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
     else {
       val text_edits = List(Text.Edit.remove(0, content.text))