23 val escape: output -> string |
23 val escape: output -> string |
24 val physical_stdout: output -> unit |
24 val physical_stdout: output -> unit |
25 val physical_stderr: output -> unit |
25 val physical_stderr: output -> unit |
26 val physical_writeln: output -> unit |
26 val physical_writeln: output -> unit |
27 exception Protocol_Message of Properties.T |
27 exception Protocol_Message of Properties.T |
28 structure Internal: |
|
29 sig |
|
30 val writeln_fn: (output -> unit) Unsynchronized.ref |
|
31 val urgent_message_fn: (output -> unit) Unsynchronized.ref |
|
32 val tracing_fn: (output -> unit) Unsynchronized.ref |
|
33 val warning_fn: (output -> unit) Unsynchronized.ref |
|
34 val error_message_fn: (serial * output -> unit) Unsynchronized.ref |
|
35 val prompt_fn: (output -> unit) Unsynchronized.ref |
|
36 val status_fn: (output -> unit) Unsynchronized.ref |
|
37 val report_fn: (output -> unit) Unsynchronized.ref |
|
38 val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref |
|
39 val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref |
|
40 end |
|
41 val urgent_message: string -> unit |
28 val urgent_message: string -> unit |
42 val error_message': serial * string -> unit |
29 val error_message': serial * string -> unit |
43 val error_message: string -> unit |
30 val error_message: string -> unit |
44 val prompt: string -> unit |
31 val prompt: string -> unit |
45 val status: string -> unit |
32 val status: string -> unit |
47 val result: Properties.T -> string -> unit |
34 val result: Properties.T -> string -> unit |
48 val protocol_message: Properties.T -> string -> unit |
35 val protocol_message: Properties.T -> string -> unit |
49 val try_protocol_message: Properties.T -> string -> unit |
36 val try_protocol_message: Properties.T -> string -> unit |
50 end; |
37 end; |
51 |
38 |
52 structure Output: OUTPUT = |
39 signature PRIVATE_OUTPUT = |
|
40 sig |
|
41 include OUTPUT |
|
42 val writeln_fn: (output -> unit) Unsynchronized.ref |
|
43 val urgent_message_fn: (output -> unit) Unsynchronized.ref |
|
44 val tracing_fn: (output -> unit) Unsynchronized.ref |
|
45 val warning_fn: (output -> unit) Unsynchronized.ref |
|
46 val error_message_fn: (serial * output -> unit) Unsynchronized.ref |
|
47 val prompt_fn: (output -> unit) Unsynchronized.ref |
|
48 val status_fn: (output -> unit) Unsynchronized.ref |
|
49 val report_fn: (output -> unit) Unsynchronized.ref |
|
50 val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref |
|
51 val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref |
|
52 end; |
|
53 |
|
54 structure Output: PRIVATE_OUTPUT = |
53 struct |
55 struct |
54 |
56 |
55 (** print modes **) |
57 (** print modes **) |
56 |
58 |
57 type output = string; (*raw system output*) |
59 type output = string; (*raw system output*) |
90 |
92 |
91 (* Isabelle output channels *) |
93 (* Isabelle output channels *) |
92 |
94 |
93 exception Protocol_Message of Properties.T; |
95 exception Protocol_Message of Properties.T; |
94 |
96 |
95 structure Internal = |
97 val writeln_fn = Unsynchronized.ref physical_writeln; |
96 struct |
98 val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s); (*Proof General legacy*) |
97 val writeln_fn = Unsynchronized.ref physical_writeln; |
99 val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s); |
98 val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s); (*Proof General legacy*) |
100 val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### "); |
99 val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s); |
101 val error_message_fn = |
100 val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### "); |
102 Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s)); |
101 val error_message_fn = |
103 val prompt_fn = Unsynchronized.ref physical_stdout; |
102 Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s)); |
104 val status_fn = Unsynchronized.ref (fn _: output => ()); |
103 val prompt_fn = Unsynchronized.ref physical_stdout; |
105 val report_fn = Unsynchronized.ref (fn _: output => ()); |
104 val status_fn = Unsynchronized.ref (fn _: output => ()); |
106 val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ()); |
105 val report_fn = Unsynchronized.ref (fn _: output => ()); |
107 val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref = |
106 val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ()); |
108 Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props); |
107 val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref = |
|
108 Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props); |
|
109 end; |
|
110 |
109 |
111 fun writeln s = ! Internal.writeln_fn (output s); |
110 fun writeln s = ! writeln_fn (output s); |
112 fun urgent_message s = ! Internal.urgent_message_fn (output s); (*Proof General legacy*) |
111 fun urgent_message s = ! urgent_message_fn (output s); (*Proof General legacy*) |
113 fun tracing s = ! Internal.tracing_fn (output s); |
112 fun tracing s = ! tracing_fn (output s); |
114 fun warning s = ! Internal.warning_fn (output s); |
113 fun warning s = ! warning_fn (output s); |
115 fun error_message' (i, s) = ! Internal.error_message_fn (i, output s); |
114 fun error_message' (i, s) = ! error_message_fn (i, output s); |
116 fun error_message s = error_message' (serial (), s); |
115 fun error_message s = error_message' (serial (), s); |
117 fun prompt s = ! Internal.prompt_fn (output s); |
116 fun prompt s = ! prompt_fn (output s); |
118 fun status s = ! Internal.status_fn (output s); |
117 fun status s = ! status_fn (output s); |
119 fun report s = ! Internal.report_fn (output s); |
118 fun report s = ! report_fn (output s); |
120 fun result props s = ! Internal.result_fn props (output s); |
119 fun result props s = ! result_fn props (output s); |
121 fun protocol_message props s = ! Internal.protocol_message_fn props (output s); |
120 fun protocol_message props s = ! protocol_message_fn props (output s); |
122 fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => (); |
121 fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => (); |
123 |
122 |
124 end; |
123 end; |
125 |
124 |
126 structure Basic_Output: BASIC_OUTPUT = Output; |
125 structure Basic_Output: BASIC_OUTPUT = Output; |