access to process output stream via auxiliary fifo;
authorwenzelm
Sat Jul 16 20:14:58 2011 +0200 (2011-07-16)
changeset 4384900f4b305687d
parent 43848 8f2bf02a0ccb
child 43850 7f2cbc713344
access to process output stream via auxiliary fifo;
src/Pure/System/isabelle_system.ML
     1.1 --- a/src/Pure/System/isabelle_system.ML	Sat Jul 16 18:41:35 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_system.ML	Sat Jul 16 20:14:58 2011 +0200
     1.3 @@ -13,6 +13,8 @@
     1.4    val create_tmp_path: string -> string -> Path.T
     1.5    val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
     1.6    val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
     1.7 +  val with_tmp_fifo: (Path.T -> 'a) -> 'a
     1.8 +  val bash_output_stream: string -> (TextIO.instream -> 'a) -> 'a
     1.9  end;
    1.10  
    1.11  structure Isabelle_System: ISABELLE_SYSTEM =
    1.12 @@ -70,5 +72,25 @@
    1.13      val _ = mkdirs path;
    1.14    in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
    1.15  
    1.16 +fun with_tmp_fifo f =
    1.17 +  with_tmp_file "isabelle-fifo-" ""
    1.18 +    (fn path =>
    1.19 +      (case bash_output ("mkfifo -m 600 " ^ File.shell_path path) of
    1.20 +        (_, 0) => f path
    1.21 +      | (out, _) => error (perhaps (try (unsuffix "\n")) out)));
    1.22 +
    1.23 +
    1.24 +(* process output stream *)
    1.25 +
    1.26 +fun bash_output_stream 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 +      | {output, ...} => error (perhaps (try (unsuffix "\n")) output))) ());
    1.35 +
    1.36  end;
    1.37