1 (* Title: Pure/General/output.ML
4 Isabelle output channels.
7 signature BASIC_OUTPUT =
9 val writeln: string -> unit
10 val tracing: string -> unit
11 val warning: string -> unit
12 val legacy_feature: string -> unit
13 val profile_time: ('a -> 'b) -> 'a -> 'b
14 val profile_time_thread: ('a -> 'b) -> 'a -> 'b
15 val profile_allocations: ('a -> 'b) -> 'a -> 'b
22 val default_output: string -> output * int
23 val default_escape: output -> string
24 val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
25 val output_width: string -> output * int
26 val output: string -> output
27 val escape: output -> string
28 val physical_stdout: output -> unit
29 val physical_stderr: output -> unit
30 val physical_writeln: output -> unit
31 type protocol_message_fn = Output_Primitives.protocol_message_fn
32 exception Protocol_Message of Properties.T
33 val protocol_message_undefined: protocol_message_fn
34 val writelns: string list -> unit
35 val state: string -> unit
36 val information: string -> unit
37 val error_message': serial * string -> unit
38 val error_message: string -> unit
39 val system_message: string -> unit
40 val status: string list -> unit
41 val report: string list -> unit
42 val result: Properties.T -> string list -> unit
43 val protocol_message: protocol_message_fn
44 val try_protocol_message: protocol_message_fn
47 signature PRIVATE_OUTPUT =
50 val writeln_fn: (output list -> unit) Unsynchronized.ref
51 val state_fn: (output list -> unit) Unsynchronized.ref
52 val information_fn: (output list -> unit) Unsynchronized.ref
53 val tracing_fn: (output list -> unit) Unsynchronized.ref
54 val warning_fn: (output list -> unit) Unsynchronized.ref
55 val legacy_fn: (output list -> unit) Unsynchronized.ref
56 val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
57 val system_message_fn: (output list -> unit) Unsynchronized.ref
58 val status_fn: (output list -> unit) Unsynchronized.ref
59 val report_fn: (output list -> unit) Unsynchronized.ref
60 val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
61 val protocol_message_fn: Output_Primitives.protocol_message_fn Unsynchronized.ref
62 val init_channels: unit -> unit
65 structure Private_Output(**): PRIVATE_OUTPUT(**) =
70 type output = string; (*raw system output*)
72 fun default_output s = (s, size s);
73 fun default_escape (s: output) = s;
76 val default = {output = default_output, escape = default_escape};
77 val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
79 fun add_mode name output escape =
80 if Thread_Data.is_virtual then ()
81 else Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
84 (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
87 fun output_width x = #output (get_mode ()) x;
88 val output = #1 o output_width;
90 fun escape x = #escape (get_mode ()) x;
94 (** output channels **)
96 (* primitives -- provided via bootstrap environment *)
98 val writeln_fn = Unsynchronized.ref Output_Primitives.writeln_fn;
99 val state_fn = Unsynchronized.ref Output_Primitives.state_fn;
100 val information_fn = Unsynchronized.ref Output_Primitives.information_fn;
101 val tracing_fn = Unsynchronized.ref Output_Primitives.tracing_fn;
102 val warning_fn = Unsynchronized.ref Output_Primitives.warning_fn;
103 val legacy_fn = Unsynchronized.ref Output_Primitives.legacy_fn;
104 val error_message_fn = Unsynchronized.ref Output_Primitives.error_message_fn;
105 val system_message_fn = Unsynchronized.ref Output_Primitives.system_message_fn;
106 val status_fn = Unsynchronized.ref Output_Primitives.status_fn;
107 val report_fn = Unsynchronized.ref Output_Primitives.report_fn;
108 val result_fn = Unsynchronized.ref Output_Primitives.result_fn;
110 type protocol_message_fn = Output_Primitives.protocol_message_fn;
111 val protocol_message_fn = Unsynchronized.ref Output_Primitives.protocol_message_fn;
114 (* physical output -- not to be used in user-space *)
116 fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
117 fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
119 fun physical_writeln "" = ()
120 | physical_writeln s = physical_stdout (suffix "\n" s); (*atomic output!*)
123 (* Isabelle output channels *)
125 exception Protocol_Message of Properties.T;
127 val protocol_message_undefined: Output_Primitives.protocol_message_fn =
128 fn props => fn _ => raise Protocol_Message props;
130 fun init_channels () =
131 (writeln_fn := (physical_writeln o implode);
132 state_fn := (fn ss => ! writeln_fn ss);
133 information_fn := Output_Primitives.ignore_outputs;
134 tracing_fn := (fn ss => ! writeln_fn ss);
135 warning_fn := (physical_writeln o prefix_lines "### " o implode);
136 legacy_fn := (fn ss => ! warning_fn ss);
137 error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
138 system_message_fn := (fn ss => ! writeln_fn ss);
139 status_fn := Output_Primitives.ignore_outputs;
140 report_fn := Output_Primitives.ignore_outputs;
141 result_fn := (fn _ => Output_Primitives.ignore_outputs);
142 protocol_message_fn := protocol_message_undefined);
144 val _ = if Thread_Data.is_virtual then () else init_channels ();
146 fun writelns ss = ! writeln_fn (map output ss);
147 fun writeln s = writelns [s];
148 fun state s = ! state_fn [output s];
149 fun information s = ! information_fn [output s];
150 fun tracing s = ! tracing_fn [output s];
151 fun warning s = ! warning_fn [output s];
152 fun legacy_feature s = ! legacy_fn [output ("Legacy feature! " ^ s)];
153 fun error_message' (i, s) = ! error_message_fn (i, [output s]);
154 fun error_message s = error_message' (serial (), s);
155 fun system_message s = ! system_message_fn [output s];
156 fun status ss = ! status_fn (map output ss);
157 (* report: string list -> unit
158 report_fn: (output list -> unit) ref*)
159 fun report ss = ! report_fn (map output ss);
161 ((** )@{print} {a = "### Private_Output.report"};( *..not yet available*)
162 (**)writeln ("### Private_Output.report " (**)^ (ss |> cat_lines |> cut_string 10)(**));
163 (* HOL build fails with greater length ----------------------------------------^^ *)
164 ! report_fn (map output ss)
166 fun result props ss = ! result_fn props (map output ss);
167 fun protocol_message props body = ! protocol_message_fn props body;
168 fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => ();
175 fun output_profile title entries =
178 |> sort (int_ord o apply2 fst)
179 |> map (fn (count, name) =>
181 val c = string_of_int count;
182 val prefix = replicate_string (Int.max (0, 10 - size c)) " ";
183 in prefix ^ c ^ " " ^ name end);
184 val total = fold (curry (op +) o fst) entries 0;
187 else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total])))
192 fun profile_time f x =
193 ML_Profiling.profile_time (output_profile "time profile:") f x;
195 fun profile_time_thread f x =
196 ML_Profiling.profile_time_thread (output_profile "time profile (this thread):") f x;
198 fun profile_allocations f x =
199 ML_Profiling.profile_allocations (output_profile "allocations profile:") f x;
206 structure Output: OUTPUT = Private_Output;
207 structure Basic_Output: BASIC_OUTPUT = Output;