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) } } }