Mercurial > isabelle
changeset 75712:048bbe0bf807
clarified signature;
author | wenzelm |
---|---|
date | Sat, 23 Jul 2022 12:19:45 +0200 |
parents | 041d7d633977 |
children | 91cdf474b64d 1d2222800ecd 14e22b525b13 |
files | src/Pure/System/isabelle_system.scala |
diffstat | 1 files changed, 24 insertions(+), 19 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Pure/System/isabelle_system.scala Sat Jul 23 11:26:28 2022 +0200 +++ b/src/Pure/System/isabelle_system.scala Sat Jul 23 12:19:45 2022 +0200 @@ -55,32 +55,37 @@ /* init settings + services */ - def get_services(): List[Class[Service]] = { - def make(where: String, names: List[String]): 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]] } - catch { - case _: ClassNotFoundException => err("Class not found") - case exn: Throwable => err(Exn.message(exn)) - } + private def init_services(where: String, names: List[String]): 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]] } + catch { + case _: ClassNotFoundException => err("Class not found") + case exn: Throwable => err(Exn.message(exn)) } } - - def from_env(variable: String): List[Class[Service]] = - make(quote(variable), space_explode(':', getenv_strict(variable))) + } - def from_jar(platform_jar: String): List[Class[Service]] = - make(quote(platform_jar), - isabelle.setup.Build.get_services(JPath.of(platform_jar)).asScala.toList) + def init_services_env(): List[Class[Service]] = + { + val variable = "ISABELLE_SCALA_SERVICES" + init_services(quote(variable), space_explode(':', getenv_strict(variable))) + } - from_env("ISABELLE_SCALA_SERVICES") ::: Scala.get_classpath().flatMap(from_jar) - } + 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(isabelle_root: String = "", cygwin_root: String = ""): Unit = { isabelle.setup.Environment.init(isabelle_root, cygwin_root) - synchronized { if (_services.isEmpty) { _services = Some(get_services()) } } + synchronized { + if (_services.isEmpty) { + _services = Some(init_services_env() ::: Scala.get_classpath().flatMap(init_services_jar)) + } + } }