20 val default_escape: output -> string |
20 val default_escape: output -> string |
21 val add_mode: string -> (string -> output * int) -> (output -> string) -> unit |
21 val add_mode: string -> (string -> output * int) -> (output -> string) -> unit |
22 val output_width: string -> output * int |
22 val output_width: string -> output * int |
23 val output: string -> output |
23 val output: string -> output |
24 val escape: output -> string |
24 val escape: output -> string |
25 val raw_stdout: output -> unit |
25 val physical_stdout: output -> unit |
26 val raw_stderr: output -> unit |
26 val physical_stderr: output -> unit |
27 val raw_writeln: output -> unit |
27 val physical_writeln: output -> unit |
28 structure Private_Hooks: |
28 structure Private_Hooks: |
29 sig |
29 sig |
30 val writeln_fn: (output -> unit) Unsynchronized.ref |
30 val writeln_fn: (output -> unit) Unsynchronized.ref |
31 val urgent_message_fn: (output -> unit) Unsynchronized.ref |
31 val urgent_message_fn: (output -> unit) Unsynchronized.ref |
32 val tracing_fn: (output -> unit) Unsynchronized.ref |
32 val tracing_fn: (output -> unit) Unsynchronized.ref |
76 |
76 |
77 (** output channels **) |
77 (** output channels **) |
78 |
78 |
79 (* raw output primitives -- not to be used in user-space *) |
79 (* raw output primitives -- not to be used in user-space *) |
80 |
80 |
81 fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); |
81 fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); |
82 fun raw_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr); |
82 fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr); |
83 |
83 |
84 fun raw_writeln "" = () |
84 fun physical_writeln "" = () |
85 | raw_writeln s = raw_stdout (suffix "\n" s); (*atomic output!*) |
85 | physical_writeln s = physical_stdout (suffix "\n" s); (*atomic output!*) |
86 |
86 |
87 |
87 |
88 (* Isabelle output channels *) |
88 (* Isabelle output channels *) |
89 |
89 |
90 structure Private_Hooks = |
90 structure Private_Hooks = |
91 struct |
91 struct |
92 val writeln_fn = Unsynchronized.ref raw_writeln; |
92 val writeln_fn = Unsynchronized.ref physical_writeln; |
93 val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s); |
93 val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s); |
94 val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s); |
94 val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s); |
95 val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### "); |
95 val warning_fn = Unsynchronized.ref (physical_stdout o suffix "\n" o prefix_lines "### "); |
96 val error_fn = |
96 val error_fn = |
97 Unsynchronized.ref (fn (_: serial, s) => raw_stdout (suffix "\n" (prefix_lines "*** " s))); |
97 Unsynchronized.ref (fn (_: serial, s) => physical_stdout (suffix "\n" (prefix_lines "*** " s))); |
98 val prompt_fn = Unsynchronized.ref raw_stdout; |
98 val prompt_fn = Unsynchronized.ref physical_stdout; |
99 val status_fn = Unsynchronized.ref (fn _: output => ()); |
99 val status_fn = Unsynchronized.ref (fn _: output => ()); |
100 val report_fn = Unsynchronized.ref (fn _: output => ()); |
100 val report_fn = Unsynchronized.ref (fn _: output => ()); |
101 val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref = |
101 val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref = |
102 Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.raw_message undefined in TTY mode"); |
102 Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.raw_message undefined in TTY mode"); |
103 end; |
103 end; |