--- 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 \
--- /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]
+}
--- 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())
}
}
--- 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)
}
--- 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)))
}
--- 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)