--- a/lib/scripts/run-polyml Tue Mar 01 13:11:56 2016 +0100
+++ b/lib/scripts/run-polyml Tue Mar 01 16:19:56 2016 +0100
@@ -43,7 +43,7 @@
PLATFORM_HEAP_FILE="$HEAP_FILE"
;;
esac
- INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.success));"
+ INIT="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.success);"
fi
--- a/src/Pure/Concurrent/bash.ML Tue Mar 01 13:11:56 2016 +0100
+++ b/src/Pure/Concurrent/bash.ML Tue Mar 01 16:19:56 2016 +0100
@@ -35,16 +35,13 @@
Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
let
val _ = File.write script_path script;
- val bash_script =
- "exec bash " ^
- File.shell_path script_path ^
- " > " ^ File.shell_path out_path ^
- " 2> " ^ File.shell_path err_path;
val _ = getenv_strict "ISABELLE_BASH_PROCESS";
val status =
OS.Process.system
("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.shell_path pid_path ^
- " bash -c " ^ quote bash_script);
+ " bash " ^ File.shell_path script_path ^
+ " > " ^ File.shell_path out_path ^
+ " 2> " ^ File.shell_path err_path);
val res =
(case Posix.Process.fromStatus status of
Posix.Process.W_EXITED => Result 0
--- a/src/Pure/Concurrent/bash_windows.ML Tue Mar 01 13:11:56 2016 +0100
+++ b/src/Pure/Concurrent/bash_windows.ML Tue Mar 01 16:19:56 2016 +0100
@@ -12,10 +12,6 @@
structure Bash: BASH =
struct
-fun cygwin_bash arg =
- let val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe"
- in Windows.simpleExecute (cmd, quote cmd ^ " -c " ^ quote arg) end;
-
val process = uninterruptible (fn restore_attributes => fn script =>
let
datatype result = Wait | Signal | Result of int;
@@ -39,12 +35,15 @@
Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
let
val _ = File.write script_path script;
+ val bash_script =
+ "bash " ^ File.shell_path script_path ^
+ " > " ^ File.shell_path out_path ^
+ " 2> " ^ File.shell_path err_path;
+ val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
val rc =
- cygwin_bash
- ("echo $$ > " ^ File.shell_path pid_path ^ "; exec bash " ^
- File.shell_path script_path ^
- " > " ^ File.shell_path out_path ^
- " 2> " ^ File.shell_path err_path)
+ 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
@@ -61,8 +60,14 @@
| terminate (SOME pid) =
let
fun kill s =
- OS.Process.isSuccess (cygwin_bash ("kill -" ^ s ^ " -" ^ string_of_int pid))
- handle OS.SysErr _ => false;
+ 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
--- a/src/Pure/Tools/build.scala Tue Mar 01 13:11:56 2016 +0100
+++ b/src/Pure/Tools/build.scala Tue Mar 01 16:19:56 2016 +0100
@@ -589,7 +589,7 @@
"$ISABELLE_PROCESS" \
-e 'use """ + quote(ml_root) + """ handle _ => OS.Process.exit OS.Process.failure;' \
-e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \
- -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
+ -q RAW_ML_SYSTEM
"""
}
else {
@@ -598,15 +598,10 @@
"$ISABELLE_PROCESS" \
-e '(use """ + quote(ml_root) + """; use "ROOT.ML") handle _ => OS.Process.exit OS.Process.failure;' \
-e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
- -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
+ -q RAW_ML_SYSTEM
"""
}
}
- else if (do_output)
- """
- rm -f "$OUTPUT"
- "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT" && chmod -w "$OUTPUT"
- """
else
"""
rm -f "$OUTPUT"