12 val copy_dir: Path.T -> Path.T -> unit |
12 val copy_dir: Path.T -> Path.T -> unit |
13 val create_tmp_path: string -> string -> Path.T |
13 val create_tmp_path: string -> string -> Path.T |
14 val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a |
14 val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a |
15 val with_tmp_dir: string -> (Path.T -> 'a) -> 'a |
15 val with_tmp_dir: string -> (Path.T -> 'a) -> 'a |
16 val with_tmp_fifo: (Path.T -> 'a) -> 'a |
16 val with_tmp_fifo: (Path.T -> 'a) -> 'a |
17 val bash_output_stream: string -> (TextIO.instream -> 'a) -> 'a |
17 val bash_output_fifo: string -> (Path.T -> 'a) -> 'a |
18 val bash_output: string -> string * int |
18 val bash_output: string -> string * int |
19 val bash: string -> int |
19 val bash: string -> int |
20 end; |
20 end; |
21 |
21 |
22 structure Isabelle_System: ISABELLE_SYSTEM = |
22 structure Isabelle_System: ISABELLE_SYSTEM = |
85 val path = create_tmp_path name ""; |
85 val path = create_tmp_path name ""; |
86 val _ = mkdirs path; |
86 val _ = mkdirs path; |
87 in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end; |
87 in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end; |
88 |
88 |
89 |
89 |
90 (* process output stream *) |
90 (* fifo *) |
91 |
91 |
92 fun with_tmp_fifo f = |
92 fun with_tmp_fifo f = |
93 with_tmp_file "isabelle-fifo-" "" |
93 with_tmp_file "isabelle-fifo-" "" |
94 (fn path => |
94 (fn path => |
95 (case bash_output ("mkfifo -m 600 " ^ File.shell_path path) of |
95 (case bash_output ("mkfifo -m 600 " ^ File.shell_path path) of |
96 (_, 0) => f path |
96 (_, 0) => f path |
97 | (out, _) => error (perhaps (try (unsuffix "\n")) out))); |
97 | (out, _) => error (perhaps (try (unsuffix "\n")) out))); |
98 |
98 |
99 fun bash_output_stream script f = |
99 fun bash_output_fifo script f = |
100 with_tmp_fifo (fn fifo => |
100 with_tmp_fifo (fn fifo => |
101 uninterruptible (fn restore_attributes => fn () => |
101 uninterruptible (fn restore_attributes => fn () => |
102 (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of |
102 (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of |
103 {rc = 0, terminate, ...} => |
103 {rc = 0, terminate, ...} => |
104 Exn.release |
104 (restore_attributes f fifo handle exn => (terminate (); reraise exn)) |
105 (Exn.capture (restore_attributes (fn () => File.open_input f fifo)) () |
|
106 before terminate ()) |
|
107 | {output, ...} => error (perhaps (try (unsuffix "\n")) output))) ()); |
105 | {output, ...} => error (perhaps (try (unsuffix "\n")) output))) ()); |
108 |
106 |
109 end; |
107 end; |
110 |
108 |