# HG changeset patch
# User wenzelm
# Date 1310840098 -7200
# Node ID 00f4b305687d360d411c8acf1f4b454d02b4e0ca
# Parent  8f2bf02a0ccbde39b79271ba0443aa986dbe8a73
access to process output stream via auxiliary fifo;

diff -r 8f2bf02a0ccb -r 00f4b305687d src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Sat Jul 16 18:41:35 2011 +0200
+++ b/src/Pure/System/isabelle_system.ML	Sat Jul 16 20:14:58 2011 +0200
@@ -13,6 +13,8 @@
   val create_tmp_path: string -> string -> Path.T
   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
+  val with_tmp_fifo: (Path.T -> 'a) -> 'a
+  val bash_output_stream: string -> (TextIO.instream -> 'a) -> 'a
 end;
 
 structure Isabelle_System: ISABELLE_SYSTEM =
@@ -70,5 +72,25 @@
     val _ = mkdirs path;
   in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
 
+fun with_tmp_fifo f =
+  with_tmp_file "isabelle-fifo-" ""
+    (fn path =>
+      (case bash_output ("mkfifo -m 600 " ^ File.shell_path path) of
+        (_, 0) => f path
+      | (out, _) => error (perhaps (try (unsuffix "\n")) out)));
+
+
+(* process output stream *)
+
+fun bash_output_stream script f =
+  with_tmp_fifo (fn fifo =>
+    uninterruptible (fn restore_attributes => fn () =>
+      (case bash_process (script ^ " > " ^ File.shell_path fifo ^ " &") of
+        {rc = 0, terminate, ...} =>
+          Exn.release
+            (Exn.capture (restore_attributes (fn () => File.open_input f fifo)) ()
+              before terminate ())
+      | {output, ...} => error (perhaps (try (unsuffix "\n")) output))) ());
+
 end;