--- 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 {
--- 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
--- 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 = () =>
{
--- 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)
{
--- 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)
}
}
}
--- 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 =
--- 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) => (),
--- 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,
--- 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)