src/Pure/Concurrent/bash_sequential.ML

--- a/src/Pure/Concurrent/bash_sequential.ML	Sat Nov 27 16:29:53 2010 +0100
+++ b/src/Pure/Concurrent/bash_sequential.ML	Sat Nov 27 19:17:55 2010 +0100
@@ -5,39 +5,30 @@
 could work via the controlling tty).
 *)
 
-local
-
-fun read_file name =
-  let val is = TextIO.openIn name
-  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
-
-fun write_file name txt =
-  let val os = TextIO.openOut name
-  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
-
-in
-
 fun bash_output script =
   let
-    val script_name = OS.FileSys.tmpName ();
-    val _ = write_file script_name script;
-
-    val output_name = OS.FileSys.tmpName ();
+    val id = serial_string ();
+    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+    val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
+    fun cleanup () = (try File.rm script_path; try File.rm output_path);
+  in
+    let
+      val _ = File.write script_path script;
+      val status =
+        OS.Process.system
+          ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
+            " script \"exec bash " ^ File.shell_path script_path ^ " > " ^
+            File.shell_path output_path ^ "\"");
+      val rc =
+        (case Posix.Process.fromStatus status of
+          Posix.Process.W_EXITED => 0
+        | Posix.Process.W_EXITSTATUS w => Word8.toInt w
+        | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
+        | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
 
-    val status =
-      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
-        " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
-    val rc =
-      (case Posix.Process.fromStatus status of
-        Posix.Process.W_EXITED => 0
-      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
-      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
-      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
+      val output = the_default "" (try File.read output_path);
+      val _ = cleanup ();
+    in (output, rc) end
+    handle exn => (cleanup (); reraise exn)
+  end;
 
-    val output = read_file output_name handle IO.Io _ => "";
-    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
-    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
-  in (output, rc) end;
-
-end;
-