| 75702 |      1 | /*  Title:      Pure/System/classpath.scala
 | 
|  |      2 |     Author:     Makarius
 | 
|  |      3 | 
 | 
|  |      4 | Java classpath and Scala services.
 | 
|  |      5 | */
 | 
|  |      6 | 
 | 
|  |      7 | package isabelle
 | 
|  |      8 | 
 | 
|  |      9 | 
 | 
|  |     10 | import java.io.{File => JFile}
 | 
|  |     11 | import java.nio.file.Files
 | 
|  |     12 | import java.net.URLClassLoader
 | 
|  |     13 | 
 | 
|  |     14 | import scala.jdk.CollectionConverters._
 | 
|  |     15 | 
 | 
|  |     16 | 
 | 
|  |     17 | object Classpath {
 | 
|  |     18 |   abstract class Service
 | 
|  |     19 |   type Service_Class = Class[Service]
 | 
|  |     20 | 
 | 
|  |     21 |   def apply(
 | 
|  |     22 |     jar_files: List[JFile] = Nil,
 | 
| 75825 |     23 |     jar_contents: List[File.Content] = Nil): Classpath =
 | 
| 75702 |     24 |   {
 | 
|  |     25 |     val jar_files0 =
 | 
|  |     26 |       for {
 | 
|  |     27 |         s <- space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
 | 
|  |     28 |         if s.nonEmpty
 | 
| 75703 |     29 |       } yield File.absolute(new JFile(s))
 | 
| 75702 |     30 | 
 | 
|  |     31 |     val jar_files1 =
 | 
| 76527 |     32 |       jar_files.flatMap(start =>
 | 
|  |     33 |           File.find_files(start, file => File.is_jar(file.getName)).sortBy(_.getName))
 | 
| 75702 |     34 |         .map(File.absolute)
 | 
|  |     35 | 
 | 
|  |     36 |     val tmp_jars =
 | 
|  |     37 |       for (jar <- jar_contents) yield {
 | 
|  |     38 |         val tmp_jar = Files.createTempFile("jar", "jar").toFile
 | 
|  |     39 |         tmp_jar.deleteOnExit()
 | 
|  |     40 |         Bytes.write(tmp_jar, jar.content)
 | 
|  |     41 |         tmp_jar
 | 
|  |     42 |       }
 | 
|  |     43 |     new Classpath(jar_files0 ::: jar_files1, tmp_jars)
 | 
|  |     44 |   }
 | 
|  |     45 | }
 | 
|  |     46 | 
 | 
|  |     47 | class Classpath private(static_jars: List[JFile], dynamic_jars: List[JFile]) {
 | 
|  |     48 |   def jars: List[JFile] = static_jars ::: dynamic_jars
 | 
|  |     49 |   override def toString: String = jars.mkString("Classpath(", ", ", ")")
 | 
|  |     50 | 
 | 
|  |     51 |   def platform_path: String = jars.map(_.getPath).mkString(JFile.pathSeparator)
 | 
|  |     52 | 
 | 
| 75704 |     53 |   val class_loader: ClassLoader =
 | 
| 75702 |     54 |   {
 | 
| 75704 |     55 |     val this_class_loader = this.getClass.getClassLoader
 | 
|  |     56 |     if (dynamic_jars.isEmpty) this_class_loader
 | 
| 75702 |     57 |     else {
 | 
| 75704 |     58 |       new URLClassLoader(dynamic_jars.map(File.url).toArray, this_class_loader) {
 | 
| 75702 |     59 |         override def finalize(): Unit = {
 | 
|  |     60 |           for (jar <- dynamic_jars) {
 | 
|  |     61 |             try { jar.delete() }
 | 
|  |     62 |             catch { case _: Throwable => }
 | 
|  |     63 |           }
 | 
|  |     64 |         }
 | 
|  |     65 |       }
 | 
|  |     66 |     }
 | 
|  |     67 |   }
 | 
|  |     68 | 
 | 
|  |     69 |   private def init_services(where: String, names: List[String]): List[Classpath.Service_Class] = {
 | 
|  |     70 |     for (name <- names) yield {
 | 
|  |     71 |       def err(msg: String): Nothing =
 | 
|  |     72 |         error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg)
 | 
| 75704 |     73 |       try { Class.forName(name, true, class_loader).asInstanceOf[Classpath.Service_Class] }
 | 
| 75702 |     74 |       catch {
 | 
|  |     75 |         case _: ClassNotFoundException => err("Class not found")
 | 
|  |     76 |         case exn: Throwable => err(Exn.message(exn))
 | 
|  |     77 |       }
 | 
|  |     78 |     }
 | 
|  |     79 |   }
 | 
|  |     80 | 
 | 
|  |     81 |   val services: List[Classpath.Service_Class] =
 | 
|  |     82 |   {
 | 
|  |     83 |     val variable = "ISABELLE_SCALA_SERVICES"
 | 
|  |     84 |     val services_env =
 | 
|  |     85 |       init_services(quote(variable), space_explode(':', Isabelle_System.getenv_strict(variable)))
 | 
|  |     86 |     val services_jars =
 | 
|  |     87 |       jars.flatMap(jar =>
 | 
|  |     88 |         init_services(File.standard_path(jar),
 | 
|  |     89 |           isabelle.setup.Build.get_services(jar.toPath).asScala.toList))
 | 
|  |     90 |     services_env ::: services_jars
 | 
|  |     91 |   }
 | 
|  |     92 | 
 | 
|  |     93 |   def make_services[C](c: Class[C]): List[C] =
 | 
|  |     94 |     for { c1 <- services if Library.is_subclass(c1, c) }
 | 
|  |     95 |       yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
 | 
|  |     96 | }
 |