# HG changeset patch
# User wenzelm
# Date 1658846351 -7200
# Node ID 6a6e90260ee7961147d11594caae174309267db4
# Parent  1b812435a63236b23056756a008209156b87dea5# Parent  21c1f82e7f5d50cf3c9c91633b2d66858b667018
merged

diff -r 1b812435a632 -r 6a6e90260ee7 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Mon Jul 25 06:31:32 2022 +0000
+++ b/src/Pure/General/path.scala	Tue Jul 26 16:39:11 2022 +0200
@@ -11,6 +11,7 @@
 import java.util.{Map => JMap}
 import java.io.{File => JFile}
 import java.nio.file.{Path => JPath}
+import java.net.{URI, URL}
 
 import scala.util.matching.Regex
 
@@ -313,6 +314,9 @@
   def is_file: Boolean = file.isFile
   def is_dir: Boolean = file.isDirectory
 
+  def uri: URI = file.toURI
+  def url: URL = uri.toURL
+
   def java_path: JPath = file.toPath
 
   def absolute_file: JFile = File.absolute(file)
diff -r 1b812435a632 -r 6a6e90260ee7 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Jul 25 06:31:32 2022 +0000
+++ b/src/Pure/System/isabelle_system.scala	Tue Jul 26 16:39:11 2022 +0200
@@ -12,6 +12,7 @@
 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._
 
@@ -48,18 +49,45 @@
     _services.get
   }
 
-  def make_services[C](c: Class[C]): List[C] =
-    for { c1 <- services() if Library.is_subclass(c1, c) }
+  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))
+    }
+  }
+
 
   /* init settings + services */
 
-  private def init_services(where: String, names: List[String]): List[Class[Service]] = {
+  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).asInstanceOf[Class[Service]] }
+      try { Class.forName(name, true, classloader).asInstanceOf[Class[Service]] }
       catch {
         case _: ClassNotFoundException => err("Class not found")
         case exn: Throwable => err(Exn.message(exn))
@@ -67,23 +95,24 @@
     }
   }
 
-  def init_services_env(): List[Class[Service]] =
+  def init_services_env(classloader: ClassLoader): List[Class[Service]] =
   {
     val variable = "ISABELLE_SCALA_SERVICES"
-    init_services(quote(variable), space_explode(':', getenv_strict(variable)))
+    init_services(quote(variable), space_explode(':', getenv_strict(variable)), classloader)
   }
 
-  def init_services_jar(jar: Path): List[Class[Service]] =
-    init_services(jar.toString, isabelle.setup.Build.get_services(jar.java_path).asScala.toList)
-
-  def init_services_jar(platform_jar: String): List[Class[Service]] =
-    init_services_jar(Path.explode(File.standard_path(platform_jar)))
+  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)
 
   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() ::: Scala.get_classpath().flatMap(init_services_jar))
+        _services =
+          Some(init_services_env(classloader) :::
+            Scala.get_classpath().flatMap(init_services_jar(_, classloader)))
       }
     }
   }
diff -r 1b812435a632 -r 6a6e90260ee7 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Mon Jul 25 06:31:32 2022 +0000
+++ b/src/Pure/System/scala.scala	Tue Jul 26 16:39:11 2022 +0200
@@ -100,9 +100,11 @@
 
   /** compiler **/
 
-  def get_classpath(): List[String] =
-    space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
-      .filter(_.nonEmpty)
+  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 {
diff -r 1b812435a632 -r 6a6e90260ee7 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon Jul 25 06:31:32 2022 +0000
+++ b/src/Pure/Thy/document_build.scala	Tue Jul 26 16:39:11 2022 +0200
@@ -155,7 +155,11 @@
 
     def get_engine(): Engine = {
       val name = document_build
-      engines.find(_.name == name).getOrElse(error("Bad document_build engine " + quote(name)))
+      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)
+        .find(_.name == name).getOrElse(error("Bad document_build engine " + quote(name)))
     }
 
     def get_export(theory: String, name: String): Export.Entry =
@@ -301,8 +305,6 @@
 
   /* build engines */
 
-  lazy val engines: List[Engine] = Isabelle_System.make_services(classOf[Engine])
-
   abstract class Engine(val name: String) extends Isabelle_System.Service {
     override def toString: String = name
 
diff -r 1b812435a632 -r 6a6e90260ee7 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Jul 25 06:31:32 2022 +0000
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Jul 26 16:39:11 2022 +0200
@@ -287,7 +287,7 @@
   def load_icon(name: String): Icon = {
     val name1 =
       if (name.startsWith("idea-icons/")) {
-        val file = Path.explode("$ISABELLE_IDEA_ICONS").file.toURI.toASCIIString
+        val file = Path.explode("$ISABELLE_IDEA_ICONS").uri.toASCIIString
         "jar:" + file + "!/" + name
       }
       else name