# HG changeset patch
# User wenzelm
# Date 1586371086 -7200
# Node ID c0bc99aad93645240cd99d87bddd77726d622767
# Parent  3d514ab74161bb21de9273480363ab8b16b811db
clarified init of settings vs. services;

diff -r 3d514ab74161 -r c0bc99aad936 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Apr 08 20:22:50 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Apr 08 20:38:06 2020 +0200
@@ -46,16 +46,28 @@
 
   /** implicit settings environment **/
 
+  abstract class Service
+
   @volatile private var _settings: Option[Map[String, String]] = None
+  @volatile private var _services: Option[List[Service]] = None
+
+  private def uninitialized: Boolean = _services.isEmpty   // unsynchronized check
 
   def settings(): Map[String, String] =
   {
-    if (_settings.isEmpty) init()  // unsynchronized check
+    if (uninitialized) init()
     _settings.get
   }
 
-  private def init_settings(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized {
-    if (_settings.isEmpty) {
+  def services(): List[Service] =
+  {
+    if (uninitialized) init()
+    _services.get
+  }
+
+  def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
+  {
+    if (uninitialized) {
       val isabelle_root1 =
         bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
 
@@ -124,18 +136,32 @@
       }
       _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]]
+              .getDeclaredConstructor().newInstance()
+          }
+          catch {
+            case _: ClassNotFoundException => err("Class not found")
+            case exn: Throwable => err(Exn.message(exn))
+          }
+        }
+      _services = Some(services)
     }
   }
 
-  def init()
-  {
-    init_settings()
-    services
-  }
-
 
   /* getenv */
 
+  private def getenv_error(name: String): Nothing =
+    error("Undefined Isabelle environment variable: " + quote(name))
+
   def getenv(name: String, env: Map[String, String] = settings()): String =
     env.getOrElse(name, "")
 
@@ -371,33 +397,6 @@
     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]].getDeclaredConstructor().newInstance()
-      }
-      catch {
-        case _: ClassNotFoundException => err("Class not found")
-        case exn: Throwable => err(Exn.message(exn))
-      }
-    }
-  }
-
-
-  /*  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 =