--- 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;
-
--- 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)
- }
- }
-}
--- 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;
--- 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"
--- 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";
--- /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;
+
--- /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)
+ }
+ }
+}
--- /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;
--- 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