# HG changeset patch
# User wenzelm
# Date 1586344445 -7200
# Node ID 6c470c918aad275bfee21ddcb41711d18ad14a66
# Parent  c986a422dee1852c8df40935e7514e7f914c9050
more general support for isabelle_scala_service;
clarified File_Format.registry;

diff -r c986a422dee1 -r 6c470c918aad NEWS
--- a/NEWS	Tue Apr 07 22:13:22 2020 +0200
+++ b/NEWS	Wed Apr 08 13:14:05 2020 +0200
@@ -12,8 +12,14 @@
 * 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); e.g. see isabelle.Bibtex.File_Format. This
+supersedes former "isabelle_file_format": minor INCOMPATIBILITY.
 
 
 
diff -r c986a422dee1 -r 6c470c918aad etc/settings
--- a/etc/settings	Tue Apr 07 22:13:22 2020 +0200
+++ b/etc/settings	Wed Apr 08 13:14:05 2020 +0200
@@ -23,7 +23,7 @@
 isabelle_scala_tools 'isabelle.Tools'
 [ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_tools '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 c986a422dee1 -r 6c470c918aad lib/scripts/getfunctions
--- a/lib/scripts/getfunctions	Tue Apr 07 22:13:22 2020 +0200
+++ b/lib/scripts/getfunctions	Wed Apr 08 13:14:05 2020 +0200
@@ -160,21 +160,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 c986a422dee1 -r 6c470c918aad src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Apr 07 22:13:22 2020 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Apr 08 13:14:05 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 c986a422dee1 -r 6c470c918aad src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Apr 07 22:13:22 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Apr 08 13:14:05 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 c986a422dee1 -r 6c470c918aad src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Apr 07 22:13:22 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Apr 08 13:14:05 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 */
 
@@ -383,6 +389,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 c986a422dee1 -r 6c470c918aad src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Tue Apr 07 22:13:22 2020 +0200
+++ b/src/Pure/Thy/file_format.scala	Wed Apr 08 13:14:05 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 c986a422dee1 -r 6c470c918aad src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Tue Apr 07 22:13:22 2020 +0200
+++ b/src/Tools/VSCode/src/document_model.scala	Wed Apr 08 13:14:05 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 c986a422dee1 -r 6c470c918aad src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Apr 07 22:13:22 2020 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Apr 08 13:14:05 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))