--- 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)))
}
}
}
--- 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