# HG changeset patch # User wenzelm # Date 1457599853 -3600 # Node ID 6cd36a0d2a289fe5ce9d1c914443a16627580aab # Parent bfa38c2e751fd25e8097c28f7b8ff3b311ebfeae clarified files; diff -r bfa38c2e751f -r 6cd36a0d2a28 src/Pure/Concurrent/bash.ML --- a/src/Pure/Concurrent/bash.ML Wed Mar 09 21:01:22 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,102 +0,0 @@ -(* Title: Pure/Concurrent/bash.ML - Author: Makarius - -GNU bash processes, with propagation of interrupts -- POSIX version. -*) - -signature BASH = -sig - val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} -end; - -structure Bash: BASH = -struct - -val process = uninterruptible (fn restore_attributes => fn script => - let - datatype result = Wait | Signal | Result of int; - val result = Synchronized.var "bash_result" Wait; - - val id = serial_string (); - val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); - val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); - val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); - val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); - - fun cleanup_files () = - (try File.rm script_path; - try File.rm out_path; - try File.rm err_path; - try File.rm pid_path); - val _ = cleanup_files (); - - val system_thread = - Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => - Multithreading.with_attributes Multithreading.private_interrupts (fn _ => - let - val _ = File.write script_path script; - val _ = getenv_strict "ISABELLE_BASH_PROCESS"; - val status = - OS.Process.system - ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^ - " bash " ^ File.bash_path script_path ^ - " > " ^ File.bash_path out_path ^ - " 2> " ^ File.bash_path err_path); - val res = - (case Posix.Process.fromStatus status of - Posix.Process.W_EXITED => Result 0 - | Posix.Process.W_EXITSTATUS 0wx82 => Signal - | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) - | Posix.Process.W_SIGNALED s => - if s = Posix.Signal.int then Signal - else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) - | Posix.Process.W_STOPPED s => - Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); - in Synchronized.change result (K res) end - handle exn => - (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); - - fun read_pid 0 = NONE - | read_pid count = - (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of - NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) - | some => some); - - fun terminate NONE = () - | terminate (SOME pid) = - let - fun kill s = - (Posix.Process.kill - (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true) - handle OS.SysErr _ => false; - - fun multi_kill count s = - count = 0 orelse - (kill s; kill (Posix.Signal.fromWord 0w0)) andalso - (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); - val _ = - multi_kill 10 Posix.Signal.int andalso - multi_kill 10 Posix.Signal.term andalso - multi_kill 10 Posix.Signal.kill; - in () end; - - fun cleanup () = - (Standard_Thread.interrupt_unsynchronized system_thread; - cleanup_files ()); - in - let - val _ = - restore_attributes (fn () => - Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); - - val out = the_default "" (try File.read out_path); - val err = the_default "" (try File.read err_path); - val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); - val pid = read_pid 1; - val _ = cleanup (); - in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end - handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) - end); - -end; - diff -r bfa38c2e751f -r 6cd36a0d2a28 src/Pure/Concurrent/bash.scala --- a/src/Pure/Concurrent/bash.scala Wed Mar 09 21:01:22 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,168 +0,0 @@ -/* Title: Pure/Concurrent/bash.scala - Author: Makarius - -GNU bash processes, with propagation of interrupts. -*/ - -package isabelle - - -import java.io.{File => JFile, BufferedReader, InputStreamReader, - BufferedWriter, OutputStreamWriter} - - -object Bash -{ - private class Limited_Progress(proc: Process, progress_limit: Option[Long]) - { - private var count = 0L - def apply(progress: String => Unit)(line: String): Unit = synchronized { - progress(line) - count = count + line.length + 1 - progress_limit match { - case Some(limit) if count > limit => proc.terminate - case _ => - } - } - } - - def process(script: String, - cwd: JFile = null, - env: Map[String, String] = Map.empty, - redirect: Boolean = false): Process = - new Process(script, cwd, env, redirect) - - class Process private [Bash]( - script: String, cwd: JFile, env: Map[String, String], redirect: Boolean) - extends Prover.System_Process - { - private val timing_file = Isabelle_System.tmp_file("bash_script") - private val timing = Synchronized[Option[Timing]](None) - - private val script_file = Isabelle_System.tmp_file("bash_script") - File.write(script_file, script) - - private val proc = - Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect, - File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", - File.standard_path(timing_file), "bash", File.standard_path(script_file)) - - - // channels - - val stdin: BufferedWriter = - new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset)) - - val stdout: BufferedReader = - new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) - - val stderr: BufferedReader = - new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) - - - // signals - - private val pid = stdout.readLine - - def interrupt() - { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } } - - private def kill(signal: String): Boolean = - Exn.Interrupt.postpone { - Isabelle_System.kill(signal, pid) - Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true - - private def multi_kill(signal: String): Boolean = - { - var running = true - var count = 10 - while (running && count > 0) { - if (kill(signal)) { - Exn.Interrupt.postpone { - Thread.sleep(100) - count -= 1 - } - } - else running = false - } - running - } - - def terminate() - { - multi_kill("INT") && multi_kill("TERM") && kill("KILL") - proc.destroy - cleanup() - } - - - // JVM shutdown hook - - private val shutdown_hook = new Thread { override def run = terminate() } - - try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } - catch { case _: IllegalStateException => } - - - // cleanup - - private def cleanup() - { - try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } - catch { case _: IllegalStateException => } - - script_file.delete - - timing.change { - case None => - if (timing_file.isFile) { - val t = - Word.explode(File.read(timing_file)) match { - case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) => - Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) - case _ => Timing.zero - } - timing_file.delete - Some(t) - } - else Some(Timing.zero) - case some => some - } - } - - - // join - - def join: Int = - { - val rc = proc.waitFor - cleanup() - rc - } - - - // result - - def result( - progress_stdout: String => Unit = (_: String) => (), - progress_stderr: String => Unit = (_: String) => (), - progress_limit: Option[Long] = None, - strict: Boolean = true): Process_Result = - { - stdin.close - - val limited = new Limited_Progress(this, progress_limit) - val out_lines = - Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) } - val err_lines = - Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) } - - val rc = - try { join } - catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } - if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() - - Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero) - } - } -} diff -r bfa38c2e751f -r 6cd36a0d2a28 src/Pure/Concurrent/bash_windows.ML --- a/src/Pure/Concurrent/bash_windows.ML Wed Mar 09 21:01:22 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,99 +0,0 @@ -(* Title: Pure/Concurrent/bash_windows.ML - Author: Makarius - -GNU bash processes, with propagation of interrupts -- Windows version. -*) - -signature BASH = -sig - val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} -end; - -structure Bash: BASH = -struct - -val process = uninterruptible (fn restore_attributes => fn script => - let - datatype result = Wait | Signal | Result of int; - val result = Synchronized.var "bash_result" Wait; - - val id = serial_string (); - val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); - val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); - val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); - val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); - - fun cleanup_files () = - (try File.rm script_path; - try File.rm out_path; - try File.rm err_path; - try File.rm pid_path); - val _ = cleanup_files (); - - val system_thread = - Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => - Multithreading.with_attributes Multithreading.private_interrupts (fn _ => - let - val _ = File.write script_path script; - val bash_script = - "bash " ^ File.bash_path script_path ^ - " > " ^ File.bash_path out_path ^ - " 2> " ^ File.bash_path err_path; - val bash_process = getenv_strict "ISABELLE_BASH_PROCESS"; - val rc = - Windows.simpleExecute ("", - quote (ML_System.platform_path bash_process) ^ " " ^ - quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script) - |> Windows.fromStatus |> SysWord.toInt; - val res = if rc = 130 orelse rc = 512 then Signal else Result rc; - in Synchronized.change result (K res) end - handle exn => - (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); - - fun read_pid 0 = NONE - | read_pid count = - (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of - NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) - | some => some); - - fun terminate NONE = () - | terminate (SOME pid) = - let - fun kill s = - let - val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe"; - val arg = "kill -" ^ s ^ " -" ^ string_of_int pid; - in - OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg)) - handle OS.SysErr _ => false - end; - - fun multi_kill count s = - count = 0 orelse - (kill s; kill "0") andalso - (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); - val _ = - multi_kill 10 "INT" andalso - multi_kill 10 "TERM" andalso - multi_kill 10 "KILL"; - in () end; - - fun cleanup () = - (Standard_Thread.interrupt_unsynchronized system_thread; - cleanup_files ()); - in - let - val _ = - restore_attributes (fn () => - Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); - - val out = the_default "" (try File.read out_path); - val err = the_default "" (try File.read err_path); - val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); - val pid = read_pid 1; - val _ = cleanup (); - in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end - handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) - end); - -end; diff -r bfa38c2e751f -r 6cd36a0d2a28 src/Pure/ROOT --- a/src/Pure/ROOT Wed Mar 09 21:01:22 2016 +0100 +++ b/src/Pure/ROOT Thu Mar 10 09:50:53 2016 +0100 @@ -3,8 +3,6 @@ session Pure = global_theories Pure files - "Concurrent/bash.ML" - "Concurrent/bash_windows.ML" "Concurrent/cache.ML" "Concurrent/counter.ML" "Concurrent/event_timer.ML" @@ -153,6 +151,8 @@ "Syntax/syntax_trans.ML" "Syntax/term_position.ML" "Syntax/type_annotation.ML" + "System/bash.ML" + "System/bash_windows.ML" "System/command_line.ML" "System/invoke_scala.ML" "System/isabelle_process.ML" diff -r bfa38c2e751f -r 6cd36a0d2a28 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Mar 09 21:01:22 2016 +0100 +++ b/src/Pure/ROOT.ML Thu Mar 10 09:50:53 2016 +0100 @@ -193,10 +193,6 @@ use "Concurrent/standard_thread.ML"; use "Concurrent/single_assignment.ML"; -if ML_System.platform_is_windows -then use "Concurrent/bash_windows.ML" -else use "Concurrent/bash.ML"; - use "Concurrent/par_exn.ML"; use "Concurrent/task_queue.ML"; use "Concurrent/future.ML"; @@ -371,8 +367,13 @@ use "Proof/proof_checker.ML"; use "Proof/extraction.ML"; +(*Isabelle system*) +if ML_System.platform_is_windows +then use "System/bash_windows.ML" +else use "System/bash.ML"; +use "System/isabelle_system.ML"; + (*theory documents*) -use "System/isabelle_system.ML"; use "Thy/term_style.ML"; use "Isar/outer_syntax.ML"; use "Thy/thy_output.ML"; diff -r bfa38c2e751f -r 6cd36a0d2a28 src/Pure/System/bash.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/bash.ML Thu Mar 10 09:50:53 2016 +0100 @@ -0,0 +1,102 @@ +(* Title: Pure/System/bash.ML + Author: Makarius + +GNU bash processes, with propagation of interrupts -- POSIX version. +*) + +signature BASH = +sig + val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} +end; + +structure Bash: BASH = +struct + +val process = uninterruptible (fn restore_attributes => fn script => + let + datatype result = Wait | Signal | Result of int; + val result = Synchronized.var "bash_result" Wait; + + val id = serial_string (); + val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); + val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); + val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); + val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); + + fun cleanup_files () = + (try File.rm script_path; + try File.rm out_path; + try File.rm err_path; + try File.rm pid_path); + val _ = cleanup_files (); + + val system_thread = + Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => + Multithreading.with_attributes Multithreading.private_interrupts (fn _ => + let + val _ = File.write script_path script; + val _ = getenv_strict "ISABELLE_BASH_PROCESS"; + val status = + OS.Process.system + ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^ + " bash " ^ File.bash_path script_path ^ + " > " ^ File.bash_path out_path ^ + " 2> " ^ File.bash_path err_path); + val res = + (case Posix.Process.fromStatus status of + Posix.Process.W_EXITED => Result 0 + | Posix.Process.W_EXITSTATUS 0wx82 => Signal + | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) + | Posix.Process.W_SIGNALED s => + if s = Posix.Signal.int then Signal + else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) + | Posix.Process.W_STOPPED s => + Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); + in Synchronized.change result (K res) end + handle exn => + (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); + + fun read_pid 0 = NONE + | read_pid count = + (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of + NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) + | some => some); + + fun terminate NONE = () + | terminate (SOME pid) = + let + fun kill s = + (Posix.Process.kill + (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true) + handle OS.SysErr _ => false; + + fun multi_kill count s = + count = 0 orelse + (kill s; kill (Posix.Signal.fromWord 0w0)) andalso + (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); + val _ = + multi_kill 10 Posix.Signal.int andalso + multi_kill 10 Posix.Signal.term andalso + multi_kill 10 Posix.Signal.kill; + in () end; + + fun cleanup () = + (Standard_Thread.interrupt_unsynchronized system_thread; + cleanup_files ()); + in + let + val _ = + restore_attributes (fn () => + Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); + + val out = the_default "" (try File.read out_path); + val err = the_default "" (try File.read err_path); + val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); + val pid = read_pid 1; + val _ = cleanup (); + in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end + handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) + end); + +end; + diff -r bfa38c2e751f -r 6cd36a0d2a28 src/Pure/System/bash.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/bash.scala Thu Mar 10 09:50:53 2016 +0100 @@ -0,0 +1,168 @@ +/* Title: Pure/System/bash.scala + Author: Makarius + +GNU bash processes, with propagation of interrupts. +*/ + +package isabelle + + +import java.io.{File => JFile, BufferedReader, InputStreamReader, + BufferedWriter, OutputStreamWriter} + + +object Bash +{ + private class Limited_Progress(proc: Process, progress_limit: Option[Long]) + { + private var count = 0L + def apply(progress: String => Unit)(line: String): Unit = synchronized { + progress(line) + count = count + line.length + 1 + progress_limit match { + case Some(limit) if count > limit => proc.terminate + case _ => + } + } + } + + def process(script: String, + cwd: JFile = null, + env: Map[String, String] = Map.empty, + redirect: Boolean = false): Process = + new Process(script, cwd, env, redirect) + + class Process private [Bash]( + script: String, cwd: JFile, env: Map[String, String], redirect: Boolean) + extends Prover.System_Process + { + private val timing_file = Isabelle_System.tmp_file("bash_script") + private val timing = Synchronized[Option[Timing]](None) + + private val script_file = Isabelle_System.tmp_file("bash_script") + File.write(script_file, script) + + private val proc = + Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect, + File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", + File.standard_path(timing_file), "bash", File.standard_path(script_file)) + + + // channels + + val stdin: BufferedWriter = + new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset)) + + val stdout: BufferedReader = + new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) + + val stderr: BufferedReader = + new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) + + + // signals + + private val pid = stdout.readLine + + def interrupt() + { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } } + + private def kill(signal: String): Boolean = + Exn.Interrupt.postpone { + Isabelle_System.kill(signal, pid) + Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true + + private def multi_kill(signal: String): Boolean = + { + var running = true + var count = 10 + while (running && count > 0) { + if (kill(signal)) { + Exn.Interrupt.postpone { + Thread.sleep(100) + count -= 1 + } + } + else running = false + } + running + } + + def terminate() + { + multi_kill("INT") && multi_kill("TERM") && kill("KILL") + proc.destroy + cleanup() + } + + + // JVM shutdown hook + + private val shutdown_hook = new Thread { override def run = terminate() } + + try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } + catch { case _: IllegalStateException => } + + + // cleanup + + private def cleanup() + { + try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } + catch { case _: IllegalStateException => } + + script_file.delete + + timing.change { + case None => + if (timing_file.isFile) { + val t = + Word.explode(File.read(timing_file)) match { + case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) => + Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) + case _ => Timing.zero + } + timing_file.delete + Some(t) + } + else Some(Timing.zero) + case some => some + } + } + + + // join + + def join: Int = + { + val rc = proc.waitFor + cleanup() + rc + } + + + // result + + def result( + progress_stdout: String => Unit = (_: String) => (), + progress_stderr: String => Unit = (_: String) => (), + progress_limit: Option[Long] = None, + strict: Boolean = true): Process_Result = + { + stdin.close + + val limited = new Limited_Progress(this, progress_limit) + val out_lines = + Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) } + val err_lines = + Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) } + + val rc = + try { join } + catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } + if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() + + Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero) + } + } +} diff -r bfa38c2e751f -r 6cd36a0d2a28 src/Pure/System/bash_windows.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/bash_windows.ML Thu Mar 10 09:50:53 2016 +0100 @@ -0,0 +1,99 @@ +(* Title: Pure/Concurrent/bash_windows.ML + Author: Makarius + +GNU bash processes, with propagation of interrupts -- Windows version. +*) + +signature BASH = +sig + val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} +end; + +structure Bash: BASH = +struct + +val process = uninterruptible (fn restore_attributes => fn script => + let + datatype result = Wait | Signal | Result of int; + val result = Synchronized.var "bash_result" Wait; + + val id = serial_string (); + val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); + val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); + val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); + val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); + + fun cleanup_files () = + (try File.rm script_path; + try File.rm out_path; + try File.rm err_path; + try File.rm pid_path); + val _ = cleanup_files (); + + val system_thread = + Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => + Multithreading.with_attributes Multithreading.private_interrupts (fn _ => + let + val _ = File.write script_path script; + val bash_script = + "bash " ^ File.bash_path script_path ^ + " > " ^ File.bash_path out_path ^ + " 2> " ^ File.bash_path err_path; + val bash_process = getenv_strict "ISABELLE_BASH_PROCESS"; + val rc = + Windows.simpleExecute ("", + quote (ML_System.platform_path bash_process) ^ " " ^ + quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script) + |> Windows.fromStatus |> SysWord.toInt; + val res = if rc = 130 orelse rc = 512 then Signal else Result rc; + in Synchronized.change result (K res) end + handle exn => + (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); + + fun read_pid 0 = NONE + | read_pid count = + (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of + NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) + | some => some); + + fun terminate NONE = () + | terminate (SOME pid) = + let + fun kill s = + let + val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe"; + val arg = "kill -" ^ s ^ " -" ^ string_of_int pid; + in + OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg)) + handle OS.SysErr _ => false + end; + + fun multi_kill count s = + count = 0 orelse + (kill s; kill "0") andalso + (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); + val _ = + multi_kill 10 "INT" andalso + multi_kill 10 "TERM" andalso + multi_kill 10 "KILL"; + in () end; + + fun cleanup () = + (Standard_Thread.interrupt_unsynchronized system_thread; + cleanup_files ()); + in + let + val _ = + restore_attributes (fn () => + Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); + + val out = the_default "" (try File.read out_path); + val err = the_default "" (try File.read err_path); + val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); + val pid = read_pid 1; + val _ = cleanup (); + in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end + handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) + end); + +end; diff -r bfa38c2e751f -r 6cd36a0d2a28 src/Pure/build-jars --- a/src/Pure/build-jars Wed Mar 09 21:01:22 2016 +0100 +++ b/src/Pure/build-jars Thu Mar 10 09:50:53 2016 +0100 @@ -9,7 +9,6 @@ ## sources declare -a SOURCES=( - Concurrent/bash.scala Concurrent/consumer_thread.scala Concurrent/counter.scala Concurrent/event_timer.scala @@ -74,6 +73,7 @@ PIDE/xml.scala PIDE/yxml.scala ROOT.scala + System/bash.scala System/command_line.scala System/cygwin.scala System/getopts.scala