# HG changeset patch
# User wenzelm
# Date 1624882313 -7200
# Node ID 6c9044f047566f5af969f33ef155432af1082fe2
# Parent  8f6b2eb15240e6b5ea3e8a0e2ab2048908e34592
clarified modules (again): services require full Isabelle/Scala environment;

diff -r 8f6b2eb15240 -r 6c9044f04756 src/Pure/System/isabelle_env.scala
--- a/src/Pure/System/isabelle_env.scala	Mon Jun 28 13:45:46 2021 +0200
+++ b/src/Pure/System/isabelle_env.scala	Mon Jun 28 14:11:53 2021 +0200
@@ -87,29 +87,17 @@
 
   /** implicit settings environment **/
 
-  abstract class Service
-
   @volatile private var _settings: Option[Map[String, String]] = None
-  @volatile private var _services: Option[List[Class[Service]]] = None
 
   def settings(): Map[String, String] =
   {
-    if (_settings.isEmpty) init()  // unsynchronized check
+    if (_settings.isEmpty) init("", "")  // unsynchronized check
     _settings.get
   }
 
-  def services(): List[Class[Service]] =
+  def init(isabelle_root: String, cygwin_root: String): Unit = synchronized
   {
-    if (_services.isEmpty) init()  // unsynchronized check
-    _services.get
-  }
-
-  def getenv_error(name: String): Nothing =
-    error("Undefined Isabelle environment variable: " + quote(name))
-
-  def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
-  {
-    if (_settings.isEmpty || _services.isEmpty) {
+    if (_settings.isEmpty) {
       val isabelle_root1 =
         bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
 
@@ -178,20 +166,6 @@
       }
       _settings = Some(settings)
       set_cygwin_root()
-
-      val variable = "ISABELLE_SCALA_SERVICES"
-      val services =
-        for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
-        yield {
-          def err(msg: String): Nothing =
-            error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
-          try { Class.forName(name).asInstanceOf[Class[Service]] }
-          catch {
-            case _: ClassNotFoundException => err("Class not found")
-            case exn: Throwable => err(Exn.message(exn))
-          }
-        }
-      _services = Some(services)
     }
   }
 }
diff -r 8f6b2eb15240 -r 6c9044f04756 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Jun 28 13:45:46 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Jun 28 14:11:53 2021 +0200
@@ -15,17 +15,6 @@
 
 object Isabelle_System
 {
-  /* services */
-
-  type Service = Isabelle_Env.Service
-
-  def services(): List[Class[Service]] = Isabelle_Env.services()
-
-  def make_services[C](c: Class[C]): List[C] =
-    for { c1 <- services() if Library.is_subclass(c1, c) }
-      yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
-
-
   /* settings */
 
   def settings(): Map[String, String] = Isabelle_Env.settings()
@@ -40,6 +29,48 @@
   def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
 
 
+  /* services */
+
+  abstract class Service
+
+  @volatile private var _services: Option[List[Class[Service]]] = None
+
+  def services(): List[Class[Service]] =
+  {
+    if (_services.isEmpty) init()  // unsynchronized check
+    _services.get
+  }
+
+  def make_services[C](c: Class[C]): List[C] =
+    for { c1 <- services() if Library.is_subclass(c1, c) }
+      yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
+
+
+  /* init settings + services */
+
+  def init(isabelle_root: String = "", cygwin_root: String = ""): Unit =
+  {
+    Isabelle_Env.init(isabelle_root, cygwin_root)
+    synchronized {
+      if (_services.isEmpty) {
+        val variable = "ISABELLE_SCALA_SERVICES"
+        val services =
+          for (name <- space_explode(':', getenv_strict(variable)))
+            yield {
+              def err(msg: String): Nothing =
+                error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
+              try { Class.forName(name).asInstanceOf[Class[Service]] }
+              catch {
+                case _: ClassNotFoundException => err("Class not found")
+                case exn: Throwable => err(Exn.message(exn))
+              }
+            }
+        _services = Some(services)
+      }
+    }
+  }
+
+
   /* getetc -- static distribution parameters */
 
   def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] =
diff -r 8f6b2eb15240 -r 6c9044f04756 src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Mon Jun 28 13:45:46 2021 +0200
+++ b/src/Pure/Tools/main.scala	Mon Jun 28 14:11:53 2021 +0200
@@ -17,13 +17,13 @@
   def main(args: Array[String]): Unit =
   {
     if (args.nonEmpty && args(0) == "-init") {
-      Isabelle_Env.init()
+      Isabelle_System.init()
     }
     else {
       val start =
       {
         try {
-          Isabelle_Env.init()
+          Isabelle_System.init()
           Isabelle_Fonts.init()
 
           GUI.init_lafs()
diff -r 8f6b2eb15240 -r 6c9044f04756 src/Tools/jEdit/src-base/plugin.scala
--- a/src/Tools/jEdit/src-base/plugin.scala	Mon Jun 28 13:45:46 2021 +0200
+++ b/src/Tools/jEdit/src-base/plugin.scala	Mon Jun 28 14:11:53 2021 +0200
@@ -17,7 +17,7 @@
 {
   override def start(): Unit =
   {
-    Isabelle_Env.init()
+    Isabelle_System.init()
 
     GUI.use_isabelle_fonts()