src/Pure/System/bash.scala
changeset 73895 b709faa96586
parent 73890 8f6b2eb15240
child 73896 5d44c6a7bd7b
equal deleted inserted replaced
73894:d7ac039421ec 73895:b709faa96586
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 
     9 
    10 import java.io.{File => JFile, BufferedReader, InputStreamReader,
    10 import java.util.{LinkedList, List => JList}
    11   BufferedWriter, OutputStreamWriter}
    11 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, File => JFile}
    12 
       
    13 import scala.annotation.tailrec
    12 import scala.annotation.tailrec
    14 import scala.jdk.OptionConverters._
    13 import scala.jdk.OptionConverters._
    15 
    14 
    16 
    15 
    17 object Bash
    16 object Bash
    48 
    47 
    49   type Watchdog = (Time, Process => Boolean)
    48   type Watchdog = (Time, Process => Boolean)
    50 
    49 
    51   def process_signal(group_pid: String, signal: String = "0"): Boolean =
    50   def process_signal(group_pid: String, signal: String = "0"): Boolean =
    52   {
    51   {
    53     val bash =
    52     val cmd = new LinkedList[String]
    54       if (Platform.is_windows) List(Isabelle_System.cygwin_root() + "\\bin\\bash.exe")
    53     if (Platform.is_windows) {
    55       else List("/usr/bin/env", "bash")
    54       cmd.add(Isabelle_System.cygwin_root() + "\\bin\\bash.exe")
    56     val (_, rc) =
    55     }
    57       Isabelle_Env.process_output(Isabelle_Env.process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
    56     else {
       
    57       cmd.add("/usr/bin/env")
       
    58       cmd.add("bash")
       
    59     }
       
    60     cmd.add("-c")
       
    61     cmd.add("kill -" + signal + " -" + group_pid)
       
    62     val (_, rc) = Isabelle_Env.process_output(Isabelle_Env.process(cmd))
    58     rc == 0
    63     rc == 0
    59   }
    64   }
    60 
    65 
    61   def process(script: String,
    66   def process(script: String,
    62       cwd: JFile = null,
    67       cwd: JFile = null,
    89     private val script_file: JFile = Isabelle_System.tmp_file("bash_script")
    94     private val script_file: JFile = Isabelle_System.tmp_file("bash_script")
    90     File.write(script_file, winpid_script)
    95     File.write(script_file, winpid_script)
    91 
    96 
    92     private val proc =
    97     private val proc =
    93       Isabelle_Env.process(
    98       Isabelle_Env.process(
    94         List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")),
    99         JList.of(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")),
    95           File.standard_path(timing_file), "bash", File.standard_path(script_file)),
   100           File.standard_path(timing_file), "bash", File.standard_path(script_file)),
    96         cwd = cwd, env = env, redirect = redirect)
   101         cwd = cwd, env = env, redirect = redirect)
    97 
   102 
    98 
   103 
    99     // channels
   104     // channels