clarified signature;
authorwenzelm
Mon, 28 Jun 2021 20:02:32 +0200
changeset 74156 b709faa96586
parent 74155 d7ac039421ec
child 74157 5d44c6a7bd7b
clarified signature;
src/Pure/System/bash.scala
src/Pure/System/isabelle_env.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)
 
--- 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)