1 (* Title: Pure/General/output.ML
2 Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
4 Output channels and timing messages.
7 signature BASIC_OUTPUT =
10 val writeln: string -> unit
11 val priority: string -> unit
12 val tracing: string -> unit
13 val warning: string -> unit
14 val tolerate_legacy_features: bool Unsynchronized.ref
15 val legacy_feature: string -> unit
16 val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
17 val timeit: (unit -> 'a) -> 'a
18 val timeap: ('a -> 'b) -> 'a -> 'b
19 val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
20 val timing: bool Unsynchronized.ref
26 val default_output: string -> output * int
27 val default_escape: output -> string
28 val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
29 val output_width: string -> output * int
30 val output: string -> output
31 val escape: output -> string
32 val std_output: output -> unit
33 val std_error: output -> unit
34 val writeln_default: output -> unit
35 val writeln_fn: (output -> unit) Unsynchronized.ref
36 val priority_fn: (output -> unit) Unsynchronized.ref
37 val tracing_fn: (output -> unit) Unsynchronized.ref
38 val warning_fn: (output -> unit) Unsynchronized.ref
39 val error_fn: (output -> unit) Unsynchronized.ref
40 val debug_fn: (output -> unit) Unsynchronized.ref
41 val prompt_fn: (output -> unit) Unsynchronized.ref
42 val status_fn: (output -> unit) Unsynchronized.ref
43 val error_msg: string -> unit
44 val prompt: string -> unit
45 val status: string -> unit
46 val debugging: bool Unsynchronized.ref
47 val no_warnings: ('a -> 'b) -> 'a -> 'b
48 val debug: (unit -> string) -> unit
51 structure Output: OUTPUT =
56 type output = string; (*raw system output*)
58 fun default_output s = (s, size s);
59 fun default_escape (s: output) = s;
62 val default = {output = default_output, escape = default_escape};
63 val modes = Unsynchronized.ref (Symtab.make [("", default)]);
65 fun add_mode name output escape = CRITICAL (fn () =>
66 Unsynchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})));
68 the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
71 fun output_width x = #output (get_mode ()) x;
72 val output = #1 o output_width;
74 fun escape x = #escape (get_mode ()) x;
78 (** output channels **)
80 (* output primitives -- normally NOT used directly!*)
82 fun std_output s = NAMED_CRITICAL "IO" (fn () =>
83 (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut));
85 fun std_error s = NAMED_CRITICAL "IO" (fn () =>
86 (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
88 fun writeln_default "" = ()
89 | writeln_default s = std_output (suffix "\n" s);
92 (* Isabelle output channels *)
94 val writeln_fn = Unsynchronized.ref writeln_default;
95 val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
96 val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
97 val warning_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "### ");
98 val error_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "*** ");
99 val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
100 val prompt_fn = Unsynchronized.ref std_output;
101 val status_fn = Unsynchronized.ref (fn _: string => ());
103 fun writeln s = ! writeln_fn (output s);
104 fun priority s = ! priority_fn (output s);
105 fun tracing s = ! tracing_fn (output s);
106 fun warning s = ! warning_fn (output s);
107 fun error_msg s = ! error_fn (output s);
108 fun prompt s = ! prompt_fn (output s);
109 fun status s = ! status_fn (output s);
111 val tolerate_legacy_features = Unsynchronized.ref true;
112 fun legacy_feature s =
113 (if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s);
115 fun no_warnings f = setmp warning_fn (K ()) f;
117 val debugging = Unsynchronized.ref false;
118 fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
124 (*conditional timing with message*)
125 fun cond_timeit flag msg e =
128 val start = start_timing ();
129 val result = Exn.capture e ();
130 val end_msg = #message (end_timing start);
131 val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
132 in Exn.release result end
135 (*unconditional timing*)
136 fun timeit e = cond_timeit true "" e;
138 (*timed application function*)
139 fun timeap f x = timeit (fn () => f x);
140 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
142 (*global timing mode*)
143 val timing = Unsynchronized.ref false;
147 structure Basic_Output: BASIC_OUTPUT = Output;