# HG changeset patch # User wenzelm # Date 1625045707 -7200 # Node ID 0ddb5de0506e075c5bd72372108c1271fd806cab # Parent 5d44c6a7bd7b4fe5926bef0018b5d2f4b3ab51ac clarified signature: prefer Java interfaces; diff -r 5d44c6a7bd7b -r 0ddb5de0506e src/Pure/General/path.scala --- a/src/Pure/General/path.scala Mon Jun 28 20:52:31 2021 +0200 +++ b/src/Pure/General/path.scala Wed Jun 30 11:35:07 2021 +0200 @@ -8,6 +8,7 @@ package isabelle +import java.util.{Map => JMap} import java.io.{File => JFile} import scala.util.matching.Regex @@ -256,7 +257,7 @@ /* expand */ - def expand_env(env: Map[String, String]): Path = + def expand_env(env: JMap[String, String]): Path = { def eval(elem: Path.Elem): List[Path.Elem] = elem match { diff -r 5d44c6a7bd7b -r 0ddb5de0506e src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Mon Jun 28 20:52:31 2021 +0200 +++ b/src/Pure/General/ssh.scala Wed Jun 30 11:35:07 2021 +0200 @@ -7,6 +7,7 @@ package isabelle +import java.util.{Map => JMap, HashMap} import java.io.{InputStream, OutputStream, ByteArrayOutputStream} import scala.collection.mutable @@ -349,10 +350,10 @@ override def close(): Unit = { sftp.disconnect; session.disconnect; on_close() } - val settings: Map[String, String] = + val settings: JMap[String, String] = { val home = sftp.getHome - Map("HOME" -> home, "USER_HOME" -> home) + JMap.of("HOME", home, "USER_HOME", home) } override def expand_path(path: Path): Path = path.expand_env(settings) def remote_path(path: Path): String = expand_path(path).implode diff -r 5d44c6a7bd7b -r 0ddb5de0506e src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Mon Jun 28 20:52:31 2021 +0200 +++ b/src/Pure/ML/ml_process.scala Wed Jun 30 11:35:07 2021 +0200 @@ -7,6 +7,7 @@ package isabelle +import java.util.{Map => JMap, HashMap} import java.io.{File => JFile} @@ -22,7 +23,7 @@ args: List[String] = Nil, modes: List[String] = Nil, cwd: JFile = null, - env: Map[String, String] = Isabelle_System.settings(), + env: JMap[String, String] = Isabelle_System.settings(), redirect: Boolean = false, cleanup: () => Unit = () => (), session_base: Option[Sessions.Base] = None): Bash.Process = @@ -70,11 +71,11 @@ if (modes.isEmpty) Nil else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes)) + // options val isabelle_process_options = Isabelle_System.tmp_file("options") Isabelle_System.chmod("600", File.path(isabelle_process_options)) File.write(isabelle_process_options, YXML.string_of_body(options.encode)) - val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") // session base @@ -99,11 +100,6 @@ // ISABELLE_TMP val isabelle_tmp = Isabelle_System.tmp_dir("process") - val env_tmp = - Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp), - "POLYSTATSDIR" -> isabelle_tmp.getAbsolutePath) - - val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(",")) val ml_runtime_options = { @@ -123,11 +119,17 @@ (eval_init ::: eval_modes ::: eval_options ::: eval_init_session).flatMap(List("--eval", _)) ::: use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args + val bash_env = new HashMap(env) + bash_env.put("ISABELLE_PROCESS_OPTIONS", File.standard_path(isabelle_process_options)) + bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp)) + bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath) + bash_env.put("ISABELLE_SCALA_FUNCTIONS", Scala.functions.mkString(",")) + Bash.process( options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + Bash.strings(bash_args), cwd = cwd, - env = env ++ env_options ++ env_tmp ++ env_functions, + env = bash_env, redirect = redirect, cleanup = () => { diff -r 5d44c6a7bd7b -r 0ddb5de0506e src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Mon Jun 28 20:52:31 2021 +0200 +++ b/src/Pure/System/bash.scala Wed Jun 30 11:35:07 2021 +0200 @@ -7,7 +7,7 @@ package isabelle -import java.util.{LinkedList, List => JList} +import java.util.{LinkedList, List => JList, Map => JMap} import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, File => JFile} import scala.annotation.tailrec import scala.jdk.OptionConverters._ @@ -64,7 +64,7 @@ def process(script: String, cwd: JFile = null, - env: Map[String, String] = Isabelle_System.settings(), + env: JMap[String, String] = Isabelle_System.settings(), redirect: Boolean = false, cleanup: () => Unit = () => ()): Process = new Process(script, cwd, env, redirect, cleanup) @@ -72,7 +72,7 @@ class Process private[Bash]( script: String, cwd: JFile, - env: Map[String, String], + env: JMap[String, String], redirect: Boolean, cleanup: () => Unit) { diff -r 5d44c6a7bd7b -r 0ddb5de0506e src/Pure/System/isabelle_env.scala --- a/src/Pure/System/isabelle_env.scala Mon Jun 28 20:52:31 2021 +0200 +++ b/src/Pure/System/isabelle_env.scala Wed Jun 30 11:35:07 2021 +0200 @@ -8,7 +8,7 @@ package isabelle -import java.util.{LinkedList, List => JList} +import java.util.{HashMap, LinkedList, List => JList, Map => JMap} import java.io.{File => JFile} import java.nio.file.Files import scala.annotation.tailrec @@ -59,39 +59,40 @@ def cygwin_init(isabelle_root: String, cygwin_root: String): Unit = { - require(Platform.is_windows, "Windows platform expected") - - def cygwin_exec(cmd: JList[String]): Unit = - { - val cwd = new JFile(isabelle_root) - val env = sys.env + ("CYGWIN" -> "nodosfilewarning") - val res = exec_process(cmd, cwd = cwd, env = env, redirect = true) - if (!res.ok) error(res.out) - } - - val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized") - val uninitialized = uninitialized_file.isFile && uninitialized_file.delete - - if (uninitialized) { - val symlinks = + if (Platform.is_windows) { + def cygwin_exec(cmd: JList[String]): Unit = { - val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath - Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]] + val cwd = new JFile(isabelle_root) + val env = new HashMap(System.getenv()) + env.put("CYGWIN", "nodosfilewarning") + val res = exec_process(cmd, cwd = cwd, env = env, redirect = true) + if (!res.ok) error(res.out) } - @tailrec def recover_symlinks(list: List[String]): Unit = - { - list match { - case Nil | List("") => - case target :: content :: rest => - cygwin_link(content, new JFile(isabelle_root, target)) - recover_symlinks(rest) - case _ => error("Unbalanced symlinks list") + + val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized") + val uninitialized = uninitialized_file.isFile && uninitialized_file.delete + + if (uninitialized) { + val symlinks = + { + val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath + Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]] } + @tailrec def recover_symlinks(list: List[String]): Unit = + { + list match { + case Nil | List("") => + case target :: content :: rest => + cygwin_link(content, new JFile(isabelle_root, target)) + recover_symlinks(rest) + case _ => error("Unbalanced symlinks list") + } + } + recover_symlinks(symlinks) + + cygwin_exec(JList.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")) + cygwin_exec(JList.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")) } - recover_symlinks(symlinks) - - cygwin_exec(JList.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")) - cygwin_exec(JList.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")) } } @@ -103,7 +104,7 @@ def process_builder(cmd: JList[String], cwd: JFile = null, - env: Map[String, String] = settings(), + env: JMap[String, String] = settings(), redirect: Boolean = false): ProcessBuilder = { val builder = new ProcessBuilder @@ -115,7 +116,7 @@ if (cwd != null) builder.directory(cwd) if (env != null) { builder.environment.clear() - for ((x, y) <- env) builder.environment.put(x, y) + builder.environment().putAll(env) } builder.redirectErrorStream(redirect) } @@ -127,7 +128,7 @@ def exec_process(command_line: JList[String], cwd: JFile = null, - env: Map[String, String] = settings(), + env: JMap[String, String] = settings(), redirect: Boolean = false): Exec_Result = { val out_file = Files.createTempFile(null, null) @@ -164,89 +165,75 @@ /** implicit settings environment **/ - @volatile private var _settings: Option[Map[String, String]] = None + @volatile private var _settings: JMap[String, String] = null - def settings(): Map[String, String] = + def settings(): JMap[String, String] = { - if (_settings.isEmpty) init("", "") // unsynchronized check - _settings.get + if (_settings == null) init("", "") // unsynchronized check + _settings } def init(isabelle_root: String, cygwin_root: String): Unit = synchronized { - if (_settings.isEmpty) { + if (_settings == null) { 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") + if (Platform.is_windows) { + val root = bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") + cygwin_init(isabelle_root1, root) + _settings = JMap.of("CYGWIN_ROOT", root) + 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)) - } + val env = new HashMap(System.getenv()) + def env_default(a: String, b: String): Unit = if (b != "") env.putIfAbsent(a, b) - 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 = + env_default("CYGWIN_ROOT", cygwin_root1) + env_default("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) - } + }) + env_default("ISABELLE_JDK_HOME", File.standard_path(jdk_home())) + env_default("HOME", System.getProperty("user.home", "")) + env_default("ISABELLE_APP", System.getProperty("isabelle.app", "")) - val settings = - { - val dump = JFile.createTempFile("settings", null) - dump.deleteOnExit - try { - val cmd = new LinkedList[String] - if (Platform.is_windows) { - cmd.add(cygwin_root1 + "\\bin\\bash") - cmd.add("-l") - cmd.add(File.standard_path(isabelle_root1 + "\\bin\\isabelle")) - } else { - cmd.add(isabelle_root1 + "/bin/isabelle") + val settings = new HashMap[String, String] + val settings_file = Files.createTempFile(null, null) + try { + val cmd = new LinkedList[String] + if (Platform.is_windows) { + cmd.add(cygwin_root1 + "\\bin\\bash") + cmd.add("-l") + cmd.add(File.standard_path(isabelle_root1 + "\\bin\\isabelle")) + } else { + cmd.add(isabelle_root1 + "/bin/isabelle") + } + cmd.add("getenv") + cmd.add("-d") + cmd.add(settings_file.toString) + + val res = exec_process(cmd, env = env, redirect = true) + if (!res.ok) error(res.out) + + for (s <- space_explode('\u0000', Files.readString(settings_file))) { + s match { + case Properties.Eq(a, b) => settings.put(a, b) + case s => if (s.nonEmpty && !s.startsWith("=")) settings.put(s, "") } - cmd.add("getenv") - cmd.add("-d") - cmd.add(dump.toString) - - val res = exec_process(cmd, env = env, redirect = true) - if (!res.ok) error(res.out) + } + } + finally { Files.delete(settings_file) } - 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() + if (Platform.is_windows) settings.put("CYGWIN_ROOT", cygwin_root1) + + settings.put("PATH", settings.get("PATH_JVM")) + settings.remove("PATH_JVM") + + _settings = JMap.copyOf(settings) } } } diff -r 5d44c6a7bd7b -r 0ddb5de0506e src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Mon Jun 28 20:52:31 2021 +0200 +++ b/src/Pure/System/isabelle_process.scala Wed Jun 30 11:35:07 2021 +0200 @@ -7,6 +7,7 @@ package isabelle +import java.util.{Map => JMap} import java.io.{File => JFile} @@ -23,7 +24,7 @@ eval_main: String = "", modes: List[String] = Nil, cwd: JFile = null, - env: Map[String, String] = Isabelle_System.settings()): Isabelle_Process = + env: JMap[String, String] = Isabelle_System.settings()): Isabelle_Process = { val channel = System_Channel() val process = diff -r 5d44c6a7bd7b -r 0ddb5de0506e src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Jun 28 20:52:31 2021 +0200 +++ b/src/Pure/System/isabelle_system.scala Wed Jun 30 11:35:07 2021 +0200 @@ -7,6 +7,7 @@ package isabelle +import java.util.{Map => JMap} import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult, StandardCopyOption, FileSystemException} @@ -17,12 +18,12 @@ { /* settings */ - def settings(): Map[String, String] = Isabelle_Env.settings() + def settings(): JMap[String, String] = Isabelle_Env.settings() - def getenv(name: String, env: Map[String, String] = settings()): String = - env.getOrElse(name, "") + def getenv(name: String, env: JMap[String, String] = settings()): String = + Option(env.get(name)).getOrElse("") - def getenv_strict(name: String, env: Map[String, String] = settings()): String = + def getenv_strict(name: String, env: JMap[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) @@ -362,7 +363,7 @@ def bash(script: String, cwd: JFile = null, - env: Map[String, String] = settings(), + env: JMap[String, String] = settings(), redirect: Boolean = false, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), diff -r 5d44c6a7bd7b -r 0ddb5de0506e src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Mon Jun 28 20:52:31 2021 +0200 +++ b/src/Pure/System/progress.scala Wed Jun 30 11:35:07 2021 +0200 @@ -7,6 +7,7 @@ package isabelle +import java.util.{Map => JMap} import java.io.{File => JFile} @@ -50,7 +51,7 @@ def bash(script: String, cwd: JFile = null, - env: Map[String, String] = Isabelle_System.settings(), + env: JMap[String, String] = Isabelle_System.settings(), redirect: Boolean = false, echo: Boolean = false, watchdog: Time = Time.zero, diff -r 5d44c6a7bd7b -r 0ddb5de0506e src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Mon Jun 28 20:52:31 2021 +0200 +++ b/src/Pure/Tools/build_job.scala Wed Jun 30 11:35:07 2021 +0200 @@ -7,6 +7,8 @@ package isabelle +import java.util.HashMap + import scala.collection.mutable @@ -217,9 +219,8 @@ val base = deps(parent) val result_base = deps(session_name) - val env = - Isabelle_System.settings() + - ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString) + val env = new HashMap(Isabelle_System.settings()) + env.put("ISABELLE_ML_DEBUGGER", options.bool("ML_debugger").toString) val is_pure = Sessions.is_pure(session_name)