# HG changeset patch
# User wenzelm
# Date 1456845596 -3600
# Node ID bd7358b3ab5ef92b71a22ed528442e98365e8a3c
# Parent  577199585ba090eb8d3d6b6c06e82362afd349be# Parent  fc353b09325d2e6939c56450c8fb76f07afb8709
merged

diff -r 577199585ba0 -r bd7358b3ab5e lib/scripts/run-polyml
--- 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
 
 
diff -r 577199585ba0 -r bd7358b3ab5e src/Pure/Concurrent/bash.ML
--- 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
diff -r 577199585ba0 -r bd7358b3ab5e src/Pure/Concurrent/bash_windows.ML
--- 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
diff -r 577199585ba0 -r bd7358b3ab5e src/Pure/Tools/build.scala
--- 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"