# HG changeset patch
# User wenzelm
# Date 1658846329 -7200
# Node ID 21c1f82e7f5d50cf3c9c91633b2d66858b667018
# Parent  c79df6dc2803d0a70652ff691ab4ae929445469b
support for dynamic classpath from exports;

diff -r c79df6dc2803 -r 21c1f82e7f5d src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Jul 25 14:40:45 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Jul 26 16:38:49 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,20 +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(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 c79df6dc2803 -r 21c1f82e7f5d src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon Jul 25 14:40:45 2022 +0200
+++ b/src/Pure/Thy/document_build.scala	Tue Jul 26 16:38:49 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