1.1 --- a/src/Pure/System/isabelle_system.ML	Sat Jul 16 20:52:41 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_system.ML	Sat Jul 16 22:17:27 2011 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
     1.5    val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
     1.6    val with_tmp_fifo: (Path.T -> 'a) -> 'a
     1.7 -  val bash_output_stream: string -> (TextIO.instream -> 'a) -> 'a
     1.8 +  val bash_output_fifo: string -> (Path.T -> 'a) -> 'a
     1.9    val bash_output: string -> string * int
    1.10    val bash: string -> int
    1.11  end;
    1.12 @@ -87,7 +87,7 @@
    1.13    in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
    1.14  
    1.15  
    1.16 -(* process output stream *)
    1.17 +(* fifo *)
    1.18  
    1.19  fun with_tmp_fifo f =
    1.20    with_tmp_file "isabelle-fifo-" ""
    1.21 @@ -96,14 +96,12 @@
    1.22          (_, 0) => f path
    1.23        | (out, _) => error (perhaps (try (unsuffix "\n")) out)));
    1.24  
    1.25 -fun bash_output_stream script f =
    1.26 +fun bash_output_fifo script f =
    1.27    with_tmp_fifo (fn fifo =>
    1.28      uninterruptible (fn restore_attributes => fn () =>
    1.29        (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of
    1.30          {rc = 0, terminate, ...} =>
    1.31 -          Exn.release
    1.32 -            (Exn.capture (restore_attributes (fn () => File.open_input f fifo)) ()
    1.33 -              before terminate ())
    1.34 +          (restore_attributes f fifo handle exn => (terminate (); reraise exn))
    1.35        | {output, ...} => error (perhaps (try (unsuffix "\n")) output))) ());
    1.36  
    1.37  end;