# HG changeset patch
# User wenzelm
# Date 1658906860 -7200
# Node ID 97e8f4c938bfba348473cf3dbe9a79cd747d88c2
# Parent  84990c95712d1626012de5e538f89d6ebd1a9149
clarified modules;

diff -r 84990c95712d -r 97e8f4c938bf etc/build.props
--- a/etc/build.props	Wed Jul 27 09:03:06 2022 +0200
+++ b/etc/build.props	Wed Jul 27 09:27:40 2022 +0200
@@ -135,6 +135,7 @@
   src/Pure/PIDE/yxml.scala \
   src/Pure/ROOT.scala \
   src/Pure/System/bash.scala \
+  src/Pure/System/classpath.scala \
   src/Pure/System/command_line.scala \
   src/Pure/System/components.scala \
   src/Pure/System/executable.scala \
diff -r 84990c95712d -r 97e8f4c938bf src/Pure/System/classpath.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/classpath.scala	Wed Jul 27 09:27:40 2022 +0200
@@ -0,0 +1,95 @@
+/*  Title:      Pure/System/classpath.scala
+    Author:     Makarius
+
+Java classpath and Scala services.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+import java.nio.file.Files
+import java.net.URLClassLoader
+
+import scala.jdk.CollectionConverters._
+
+
+object Classpath {
+  abstract class Service
+  type Service_Class = Class[Service]
+
+  def apply(
+    jar_files: List[JFile] = Nil,
+    jar_contents: List[File.Content_Bytes] = Nil): Classpath =
+  {
+    val jar_files0 =
+      for {
+        s <- space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
+        if s.nonEmpty
+      } yield new JFile(s)
+
+    val jar_files1 =
+      jar_files.flatMap(start => File.find_files(start, _.getName.endsWith(".jar")))
+        .map(File.absolute)
+
+    val tmp_jars =
+      for (jar <- jar_contents) yield {
+        val tmp_jar = Files.createTempFile("jar", "jar").toFile
+        tmp_jar.deleteOnExit()
+        Bytes.write(tmp_jar, jar.content)
+        tmp_jar
+      }
+    new Classpath(jar_files0 ::: jar_files1, tmp_jars)
+  }
+}
+
+class Classpath private(static_jars: List[JFile], dynamic_jars: List[JFile]) {
+  def jars: List[JFile] = static_jars ::: dynamic_jars
+  override def toString: String = jars.mkString("Classpath(", ", ", ")")
+
+  def platform_path: String = jars.map(_.getPath).mkString(JFile.pathSeparator)
+
+  val classloader: ClassLoader =
+  {
+    val this_classloader = this.getClass.getClassLoader
+    if (dynamic_jars.isEmpty) this_classloader
+    else {
+      new URLClassLoader(dynamic_jars.map(File.url).toArray, this_classloader) {
+        override def finalize(): Unit = {
+          for (jar <- dynamic_jars) {
+            try { jar.delete() }
+            catch { case _: Throwable => }
+          }
+        }
+      }
+    }
+  }
+
+  private def init_services(where: String, names: List[String]): List[Classpath.Service_Class] = {
+    for (name <- names) yield {
+      def err(msg: String): Nothing =
+        error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg)
+      try { Class.forName(name, true, classloader).asInstanceOf[Classpath.Service_Class] }
+      catch {
+        case _: ClassNotFoundException => err("Class not found")
+        case exn: Throwable => err(Exn.message(exn))
+      }
+    }
+  }
+
+  val services: List[Classpath.Service_Class] =
+  {
+    val variable = "ISABELLE_SCALA_SERVICES"
+    val services_env =
+      init_services(quote(variable), space_explode(':', Isabelle_System.getenv_strict(variable)))
+    val services_jars =
+      jars.flatMap(jar =>
+        init_services(File.standard_path(jar),
+          isabelle.setup.Build.get_services(jar.toPath).asScala.toList))
+    services_env ::: services_jars
+  }
+
+  def make_services[C](c: Class[C]): List[C] =
+    for { c1 <- services if Library.is_subclass(c1, c) }
+      yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
+}
diff -r 84990c95712d -r 97e8f4c938bf src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Jul 27 09:03:06 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Jul 27 09:27:40 2022 +0200
@@ -12,9 +12,6 @@
 import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
   StandardCopyOption, FileSystemException}
 import java.nio.file.attribute.BasicFileAttributes
-import java.net.URLClassLoader
-
-import scala.jdk.CollectionConverters._
 
 
 object Isabelle_System {
@@ -40,80 +37,24 @@
 
   /* services */
 
-  abstract class Service
+  type Service = Classpath.Service
 
-  @volatile private var _services: Option[List[Class[Service]]] = None
+  @volatile private var _classpath: Option[Classpath] = None
 
-  def services(): List[Class[Service]] = {
-    if (_services.isEmpty) init()  // unsynchronized check
-    _services.get
+  def classpath(): Classpath = {
+    if (_classpath.isEmpty) init()  // unsynchronized check
+    _classpath.get
   }
 
-  def make_services[C](c: Class[C], more_services: List[Class[Service]] = Nil): List[C] =
-    for { c1 <- services() ::: more_services if Library.is_subclass(c1, c) }
-      yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
-
-  class Tmp_Loader private[Isabelle_System](tmp_jars: List[JFile], parent: ClassLoader)
-    extends URLClassLoader(tmp_jars.map(_.toURI.toURL).toArray, parent) {
-      override def finalize(): Unit = {
-        for (tmp_jar <- tmp_jars) {
-          try { tmp_jar.delete() }
-          catch { case _: Throwable => }
-        }
-      }
-    }
-
-  def make_classloader(jars: List[File.Content_Bytes]): (List[JFile], ClassLoader) =
-  {
-    val default_classloader = Isabelle_System.getClass.getClassLoader
-    if (jars.isEmpty) (Nil, default_classloader)
-    else {
-      val tmp_jars =
-        for (jar <- jars) yield {
-          val tmp_jar = tmp_file("jar", ext = "jar")
-          Bytes.write(tmp_jar, jar.content)
-          tmp_jar
-        }
-      (tmp_jars, new Tmp_Loader(tmp_jars, default_classloader))
-    }
-  }
+  def make_services[C](c: Class[C]): List[C] = classpath().make_services(c)
 
 
-  /* init settings + services */
-
-  private def init_services(
-    where: String, names: List[String], classloader: ClassLoader
-  ): List[Class[Service]] = {
-    for (name <- names) yield {
-      def err(msg: String): Nothing =
-        error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg)
-      try { Class.forName(name, true, classloader).asInstanceOf[Class[Service]] }
-      catch {
-        case _: ClassNotFoundException => err("Class not found")
-        case exn: Throwable => err(Exn.message(exn))
-      }
-    }
-  }
-
-  def init_services_env(classloader: ClassLoader): List[Class[Service]] =
-  {
-    val variable = "ISABELLE_SCALA_SERVICES"
-    init_services(quote(variable), space_explode(':', getenv_strict(variable)), classloader)
-  }
-
-  def init_services_jar(jar: Path, classloader: ClassLoader): List[Class[Service]] =
-    init_services(jar.toString,
-      isabelle.setup.Build.get_services(jar.java_path).asScala.toList, classloader)
+  /* init settings + classpath */
 
   def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = {
     isabelle.setup.Environment.init(isabelle_root, cygwin_root)
-    val (_, classloader) = make_classloader(Nil)
     synchronized {
-      if (_services.isEmpty) {
-        _services =
-          Some(init_services_env(classloader) :::
-            Scala.get_classpath().flatMap(init_services_jar(_, classloader)))
-      }
+      if (_classpath.isEmpty) _classpath = Some(Classpath())
     }
   }
 
diff -r 84990c95712d -r 97e8f4c938bf src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Wed Jul 27 09:03:06 2022 +0200
+++ b/src/Pure/System/scala.scala	Wed Jul 27 09:27:40 2022 +0200
@@ -100,12 +100,6 @@
 
   /** compiler **/
 
-  def get_classpath(): List[Path] =
-    for {
-      s <- space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
-      if s.nonEmpty
-    } yield Path.explode(File.standard_path(s))
-
   object Compiler {
     object Message {
       object Kind extends Enumeration {
@@ -164,19 +158,13 @@
 
     def context(
       settings: List[String] = Nil,
-      jar_dirs: List[JFile] = Nil,
+      jar_files: List[JFile] = Nil,
       class_loader: Option[ClassLoader] = None
     ): Context = {
       val isabelle_settings =
         Word.explode(Isabelle_System.getenv_strict("ISABELLE_SCALAC_OPTIONS"))
 
-      def find_jars(dir: JFile): List[String] =
-        File.find_files(dir, file => file.getName.endsWith(".jar")).
-          map(File.absolute_name)
-
-      val classpath =
-        (get_classpath().map(File.platform_path) :::
-          jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
+      val classpath = Classpath(jar_files = jar_files).platform_path
       val settings1 = isabelle_settings ::: settings ::: List("-classpath", classpath)
       new Context(settings1, class_loader)
     }
diff -r 84990c95712d -r 97e8f4c938bf src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Wed Jul 27 09:03:06 2022 +0200
+++ b/src/Pure/Thy/document_build.scala	Wed Jul 27 09:27:40 2022 +0200
@@ -155,10 +155,7 @@
 
     def get_engine(): Engine = {
       val name = document_build
-      val (files, classloader) = Isabelle_System.make_classloader(classpath)
-      val more_services =
-        files.flatMap(file => Isabelle_System.init_services_jar(File.path(file), classloader))
-      Isabelle_System.make_services(classOf[Engine], more_services = more_services)
+      Classpath(jar_contents = classpath).make_services(classOf[Engine])
         .find(_.name == name).getOrElse(error("Bad document_build engine " + quote(name)))
     }
 
diff -r 84990c95712d -r 97e8f4c938bf src/Tools/jEdit/jedit_main/scala_console.scala
--- a/src/Tools/jEdit/jedit_main/scala_console.scala	Wed Jul 27 09:03:06 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/scala_console.scala	Wed Jul 27 09:27:40 2022 +0200
@@ -90,7 +90,7 @@
   override def openConsole(console: Console): Unit = {
     val context =
       Scala.Compiler.context(
-      jar_dirs = JEdit_Lib.directories,
+      jar_files = JEdit_Lib.directories,
       class_loader = Some(new JARClassLoader))
 
     val interpreter = new Scala_Console.Interpreter(context, console)