# HG changeset patch # User wenzelm # Date 1624880746 -7200 # Node ID 8f6b2eb15240e6b5ea3e8a0e2ab2048908e34592 # Parent 5ec68c1a07d82ae79410f0e8a422e6995a909f62 clarified modules; diff -r 5ec68c1a07d8 -r 8f6b2eb15240 src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Mon Jun 28 13:13:31 2021 +0200 +++ b/src/Pure/System/bash.scala Mon Jun 28 13:45:46 2021 +0200 @@ -48,6 +48,16 @@ type Watchdog = (Time, Process => Boolean) + def process_signal(group_pid: String, signal: String = "0"): Boolean = + { + val bash = + if (Platform.is_windows) List(Isabelle_System.cygwin_root() + "\\bin\\bash.exe") + else List("/usr/bin/env", "bash") + val (_, rc) = + Isabelle_Env.process_output(Isabelle_Env.process(bash ::: List("-c", "kill -" + signal + " -" + group_pid))) + rc == 0 + } + def process(script: String, cwd: JFile = null, env: Map[String, String] = Isabelle_System.settings(), @@ -80,7 +90,7 @@ File.write(script_file, winpid_script) private val proc = - Isabelle_System.process( + Isabelle_Env.process( List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), File.standard_path(timing_file), "bash", File.standard_path(script_file)), cwd = cwd, env = env, redirect = redirect) @@ -119,8 +129,8 @@ { count <= 0 || { - Isabelle_System.process_signal(group_pid, signal = s) - val running = root_process_alive() || Isabelle_System.process_signal(group_pid) + process_signal(group_pid, signal = s) + val running = root_process_alive() || process_signal(group_pid) if (running) { Time.seconds(0.1).sleep() signal(s, count - 1) @@ -138,7 +148,7 @@ def interrupt(): Unit = Isabelle_Thread.try_uninterruptible { - Isabelle_System.process_signal(group_pid, "INT") + process_signal(group_pid, "INT") } diff -r 5ec68c1a07d8 -r 8f6b2eb15240 src/Pure/System/cygwin.scala --- a/src/Pure/System/cygwin.scala Mon Jun 28 13:13:31 2021 +0200 +++ b/src/Pure/System/cygwin.scala Mon Jun 28 13:45:46 2021 +0200 @@ -25,8 +25,8 @@ { val cwd = new JFile(isabelle_root) val env = sys.env + ("CYGWIN" -> "nodosfilewarning") - val proc = Isabelle_System.process(cmdline.toList, cwd = cwd, env = env, redirect = true) - val (output, rc) = Isabelle_System.process_output(proc) + val proc = Isabelle_Env.process(cmdline.toList, cwd = cwd, env = env, redirect = true) + val (output, rc) = Isabelle_Env.process_output(proc) if (rc != 0) error(output) } diff -r 5ec68c1a07d8 -r 8f6b2eb15240 src/Pure/System/isabelle_env.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/isabelle_env.scala Mon Jun 28 13:45:46 2021 +0200 @@ -0,0 +1,197 @@ +/* Title: Pure/System/isabelle_env.scala + Author: Makarius + +Fundamental Isabelle system environment: quasi-static module with +optional init operation. +*/ + +package isabelle + + +import java.io.{File => JFile} + +import scala.jdk.CollectionConverters._ + + + +object Isabelle_Env +{ + /** bootstrap information **/ + + def jdk_home(): String = + { + val java_home = System.getProperty("java.home", "") + val home = new JFile(java_home) + val parent = home.getParent + if (home.getName == "jre" && parent != null && + (new JFile(new JFile(parent, "bin"), "javac")).exists) parent + else java_home + } + + def bootstrap_directory( + preference: String, envar: String, property: String, description: String): String = + { + val value = + proper_string(preference) orElse // explicit argument + proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool + proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process + error("Unknown " + description + " directory") + + if ((new JFile(value)).isDirectory) value + else error("Bad " + description + " directory " + quote(value)) + } + + + + /** raw process **/ + + /* raw process */ + + def process(command_line: List[String], + cwd: JFile = null, + env: Map[String, String] = settings(), + redirect: Boolean = false): Process = + { + val proc = new ProcessBuilder + + // fragile on Windows: + // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160 + proc.command(command_line.asJava) + + if (cwd != null) proc.directory(cwd) + if (env != null) { + proc.environment.clear() + for ((x, y) <- env) proc.environment.put(x, y) + } + proc.redirectErrorStream(redirect) + proc.start + } + + def process_output(proc: Process): (String, Int) = + { + proc.getOutputStream.close() + + val output = File.read_stream(proc.getInputStream) + val rc = + try { proc.waitFor } + finally { + proc.getInputStream.close() + proc.getErrorStream.close() + proc.destroy() + Exn.Interrupt.dispose() + } + (output, rc) + } + + + + /** implicit settings environment **/ + + abstract class Service + + @volatile private var _settings: Option[Map[String, String]] = None + @volatile private var _services: Option[List[Class[Service]]] = None + + def settings(): Map[String, String] = + { + if (_settings.isEmpty) init() // unsynchronized check + _settings.get + } + + def services(): List[Class[Service]] = + { + if (_services.isEmpty) init() // unsynchronized check + _services.get + } + + def getenv_error(name: String): Nothing = + error("Undefined Isabelle environment variable: " + quote(name)) + + def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized + { + if (_settings.isEmpty || _services.isEmpty) { + val isabelle_root1 = + bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root") + + val cygwin_root1 = + if (Platform.is_windows) + bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") + else "" + + if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1) + + def set_cygwin_root(): Unit = + { + if (Platform.is_windows) + _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1)) + } + + set_cygwin_root() + + def default(env: Map[String, String], entry: (String, String)): Map[String, String] = + if (env.isDefinedAt(entry._1) || entry._2 == "") env + else env + entry + + val env = + { + val temp_windows = + { + val temp = if (Platform.is_windows) System.getenv("TEMP") else null + if (temp != null && temp.contains('\\')) temp else "" + } + val user_home = System.getProperty("user.home", "") + val isabelle_app = System.getProperty("isabelle.app", "") + + default( + default( + default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), + "TEMP_WINDOWS" -> temp_windows), + "HOME" -> user_home), + "ISABELLE_APP" -> isabelle_app) + } + + val settings = + { + val dump = JFile.createTempFile("settings", null) + dump.deleteOnExit + try { + val cmd1 = + if (Platform.is_windows) + List(cygwin_root1 + "\\bin\\bash", "-l", + File.standard_path(isabelle_root1 + "\\bin\\isabelle")) + else + List(isabelle_root1 + "/bin/isabelle") + val cmd = cmd1 ::: List("getenv", "-d", dump.toString) + + val (output, rc) = process_output(process(cmd, env = env, redirect = true)) + if (rc != 0) error(output) + + val entries = + space_explode('\u0000', File.read(dump)).flatMap( + { + case Properties.Eq(a, b) => Some(a -> b) + case s => if (s.isEmpty || s.startsWith("=")) None else Some(s -> "") + }).toMap + entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" + } + finally { dump.delete } + } + _settings = Some(settings) + set_cygwin_root() + + val variable = "ISABELLE_SCALA_SERVICES" + val services = + for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable)))) + yield { + def err(msg: String): Nothing = + error("Bad entry " + quote(name) + " in " + variable + "\n" + msg) + try { Class.forName(name).asInstanceOf[Class[Service]] } + catch { + case _: ClassNotFoundException => err("Class not found") + case exn: Throwable => err(Exn.message(exn)) + } + } + _services = Some(services) + } + } +} diff -r 5ec68c1a07d8 -r 8f6b2eb15240 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Jun 28 13:13:31 2021 +0200 +++ b/src/Pure/System/isabelle_system.scala Mon Jun 28 13:45:46 2021 +0200 @@ -1,8 +1,7 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius -Fundamental Isabelle system environment: quasi-static module with -optional init operation. +Miscellaneous Isabelle system operations. */ package isabelle @@ -13,154 +12,23 @@ StandardCopyOption, FileSystemException} import java.nio.file.attribute.BasicFileAttributes -import scala.jdk.CollectionConverters._ - object Isabelle_System { - /** bootstrap information **/ - - def jdk_home(): String = - { - val java_home = System.getProperty("java.home", "") - val home = new JFile(java_home) - val parent = home.getParent - if (home.getName == "jre" && parent != null && - (new JFile(new JFile(parent, "bin"), "javac")).exists) parent - else java_home - } - - def bootstrap_directory( - preference: String, envar: String, property: String, description: String): String = - { - val value = - proper_string(preference) orElse // explicit argument - proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool - proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process - error("Unknown " + description + " directory") + /* services */ - if ((new JFile(value)).isDirectory) value - else error("Bad " + description + " directory " + quote(value)) - } - - - - /** implicit settings environment **/ - - abstract class Service + type Service = Isabelle_Env.Service - @volatile private var _settings: Option[Map[String, String]] = None - @volatile private var _services: Option[List[Class[Service]]] = None - - def settings(): Map[String, String] = - { - if (_settings.isEmpty) init() // unsynchronized check - _settings.get - } - - def services(): List[Class[Service]] = - { - if (_services.isEmpty) init() // unsynchronized check - _services.get - } + def services(): List[Class[Service]] = Isabelle_Env.services() def make_services[C](c: Class[C]): List[C] = for { c1 <- services() if Library.is_subclass(c1, c) } yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C] - def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized - { - if (_settings.isEmpty || _services.isEmpty) { - val isabelle_root1 = - bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root") - - val cygwin_root1 = - if (Platform.is_windows) - bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") - else "" - - if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1) - - def set_cygwin_root(): Unit = - { - if (Platform.is_windows) - _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1)) - } - - set_cygwin_root() - - def default(env: Map[String, String], entry: (String, String)): Map[String, String] = - if (env.isDefinedAt(entry._1) || entry._2 == "") env - else env + entry - - val env = - { - val temp_windows = - { - val temp = if (Platform.is_windows) System.getenv("TEMP") else null - if (temp != null && temp.contains('\\')) temp else "" - } - val user_home = System.getProperty("user.home", "") - val isabelle_app = System.getProperty("isabelle.app", "") - - default( - default( - default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), - "TEMP_WINDOWS" -> temp_windows), - "HOME" -> user_home), - "ISABELLE_APP" -> isabelle_app) - } - val settings = - { - val dump = JFile.createTempFile("settings", null) - dump.deleteOnExit - try { - val cmd1 = - if (Platform.is_windows) - List(cygwin_root1 + "\\bin\\bash", "-l", - File.standard_path(isabelle_root1 + "\\bin\\isabelle")) - else - List(isabelle_root1 + "/bin/isabelle") - val cmd = cmd1 ::: List("getenv", "-d", dump.toString) - - val (output, rc) = process_output(process(cmd, env = env, redirect = true)) - if (rc != 0) error(output) + /* settings */ - val entries = - space_explode('\u0000', File.read(dump)).flatMap( - { - case Properties.Eq(a, b) => Some(a -> b) - case s => if (s.isEmpty || s.startsWith("=")) None else Some(s -> "") - }).toMap - entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" - } - finally { dump.delete } - } - _settings = Some(settings) - set_cygwin_root() - - val variable = "ISABELLE_SCALA_SERVICES" - val services = - for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable)))) - yield { - def err(msg: String): Nothing = - error("Bad entry " + quote(name) + " in " + variable + "\n" + msg) - try { Class.forName(name).asInstanceOf[Class[Service]] } - catch { - case _: ClassNotFoundException => err("Class not found") - case exn: Throwable => err(Exn.message(exn)) - } - } - _services = Some(services) - } - } - - - /* getenv -- dynamic process environment */ - - private def getenv_error(name: String): Nothing = - error("Undefined Isabelle environment variable: " + quote(name)) + def settings(): Map[String, String] = Isabelle_Env.settings() def getenv(name: String, env: Map[String, String] = settings()): String = env.getOrElse(name, "") @@ -458,54 +326,6 @@ /** external processes **/ - /* raw process */ - - def process(command_line: List[String], - cwd: JFile = null, - env: Map[String, String] = settings(), - redirect: Boolean = false): Process = - { - val proc = new ProcessBuilder - - // fragile on Windows: - // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160 - proc.command(command_line.asJava) - - if (cwd != null) proc.directory(cwd) - if (env != null) { - proc.environment.clear() - for ((x, y) <- env) proc.environment.put(x, y) - } - proc.redirectErrorStream(redirect) - proc.start - } - - def process_output(proc: Process): (String, Int) = - { - proc.getOutputStream.close() - - val output = File.read_stream(proc.getInputStream) - val rc = - try { proc.waitFor } - finally { - proc.getInputStream.close() - proc.getErrorStream.close() - proc.destroy() - Exn.Interrupt.dispose() - } - (output, rc) - } - - def process_signal(group_pid: String, signal: String = "0"): Boolean = - { - val bash = - if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe") - else List("/usr/bin/env", "bash") - val (_, rc) = process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid))) - rc == 0 - } - - /* GNU bash */ def bash(script: String, diff -r 5ec68c1a07d8 -r 8f6b2eb15240 src/Pure/Tools/main.scala --- a/src/Pure/Tools/main.scala Mon Jun 28 13:13:31 2021 +0200 +++ b/src/Pure/Tools/main.scala Mon Jun 28 13:45:46 2021 +0200 @@ -17,13 +17,13 @@ def main(args: Array[String]): Unit = { if (args.nonEmpty && args(0) == "-init") { - Isabelle_System.init() + Isabelle_Env.init() } else { val start = { try { - Isabelle_System.init() + Isabelle_Env.init() Isabelle_Fonts.init() GUI.init_lafs() diff -r 5ec68c1a07d8 -r 8f6b2eb15240 src/Pure/build-jars --- a/src/Pure/build-jars Mon Jun 28 13:13:31 2021 +0200 +++ b/src/Pure/build-jars Mon Jun 28 13:45:46 2021 +0200 @@ -137,6 +137,7 @@ src/Pure/System/executable.scala src/Pure/System/getopts.scala src/Pure/System/isabelle_charset.scala + src/Pure/System/isabelle_env.scala src/Pure/System/isabelle_fonts.scala src/Pure/System/isabelle_platform.scala src/Pure/System/isabelle_process.scala diff -r 5ec68c1a07d8 -r 8f6b2eb15240 src/Tools/jEdit/src-base/plugin.scala --- a/src/Tools/jEdit/src-base/plugin.scala Mon Jun 28 13:13:31 2021 +0200 +++ b/src/Tools/jEdit/src-base/plugin.scala Mon Jun 28 13:45:46 2021 +0200 @@ -17,7 +17,7 @@ { override def start(): Unit = { - Isabelle_System.init() + Isabelle_Env.init() GUI.use_isabelle_fonts()