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