# HG changeset patch # User wenzelm # Date 1624903352 -7200 # Node ID b709faa9658677a50e960a927bdd4ce0bd2484ff # Parent d7ac039421ece0853bab6c25a0b8f9f4a79b73b8 clarified signature; diff -r d7ac039421ec -r b709faa96586 src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Mon Jun 28 18:10:06 2021 +0200 +++ b/src/Pure/System/bash.scala Mon Jun 28 20:02:32 2021 +0200 @@ -7,9 +7,8 @@ package isabelle -import java.io.{File => JFile, BufferedReader, InputStreamReader, - BufferedWriter, OutputStreamWriter} - +import java.util.{LinkedList, List => JList} +import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, File => JFile} import scala.annotation.tailrec import scala.jdk.OptionConverters._ @@ -50,11 +49,17 @@ 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))) + val cmd = new LinkedList[String] + if (Platform.is_windows) { + cmd.add(Isabelle_System.cygwin_root() + "\\bin\\bash.exe") + } + else { + cmd.add("/usr/bin/env") + cmd.add("bash") + } + cmd.add("-c") + cmd.add("kill -" + signal + " -" + group_pid) + val (_, rc) = Isabelle_Env.process_output(Isabelle_Env.process(cmd)) rc == 0 } @@ -91,7 +96,7 @@ private val proc = Isabelle_Env.process( - List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), + JList.of(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) diff -r d7ac039421ec -r b709faa96586 src/Pure/System/isabelle_env.scala --- a/src/Pure/System/isabelle_env.scala Mon Jun 28 18:10:06 2021 +0200 +++ b/src/Pure/System/isabelle_env.scala Mon Jun 28 20:02:32 2021 +0200 @@ -8,10 +8,9 @@ package isabelle +import java.util.{LinkedList, List => JList} import java.io.{File => JFile} import java.nio.file.Files - -import scala.jdk.CollectionConverters._ import scala.annotation.tailrec @@ -62,12 +61,12 @@ { require(Platform.is_windows, "Windows platform expected") - def exec(cmdline: String*): Unit = + def exec(cmdline: JList[String]): Unit = { val cwd = new JFile(isabelle_root) val env = sys.env + ("CYGWIN" -> "nodosfilewarning") - val proc = Isabelle_Env.process(cmdline.toList, cwd = cwd, env = env, redirect = true) - val (output, rc) = Isabelle_Env.process_output(proc) + val (output, rc) = + Isabelle_Env.process_output(Isabelle_Env.process(cmdline, cwd = cwd, env = env, redirect = true)) if (rc != 0) error(output) } @@ -92,8 +91,8 @@ } recover_symlinks(symlinks) - exec(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall") - exec(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall") + exec(JList.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")) + exec(JList.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")) } } @@ -103,7 +102,7 @@ /* raw process */ - def process(command_line: List[String], + def process(command_line: JList[String], cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false): Process = @@ -112,7 +111,7 @@ // 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) + proc.command(command_line) if (cwd != null) proc.directory(cwd) if (env != null) { @@ -199,13 +198,17 @@ 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 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(dump.toString) val (output, rc) = process_output(process(cmd, env = env, redirect = true)) if (rc != 0) error(output)