wenzelm@14815
|
1 |
(* Title: Pure/General/output.ML
|
wenzelm@14815
|
2 |
Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
|
wenzelm@14815
|
3 |
|
wenzelm@42883
|
4 |
Isabelle output channels.
|
wenzelm@14815
|
5 |
*)
|
wenzelm@14815
|
6 |
|
wenzelm@14815
|
7 |
signature BASIC_OUTPUT =
|
wenzelm@14815
|
8 |
sig
|
wenzelm@18682
|
9 |
val writeln: string -> unit
|
wenzelm@18682
|
10 |
val tracing: string -> unit
|
wenzelm@18682
|
11 |
val warning: string -> unit
|
wenzelm@14815
|
12 |
end;
|
wenzelm@14815
|
13 |
|
wenzelm@14815
|
14 |
signature OUTPUT =
|
wenzelm@14815
|
15 |
sig
|
wenzelm@14815
|
16 |
include BASIC_OUTPUT
|
wenzelm@40391
|
17 |
type output = string
|
wenzelm@23660
|
18 |
val default_output: string -> output * int
|
wenzelm@23660
|
19 |
val default_escape: output -> string
|
wenzelm@23660
|
20 |
val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
|
wenzelm@23660
|
21 |
val output_width: string -> output * int
|
wenzelm@23660
|
22 |
val output: string -> output
|
wenzelm@23660
|
23 |
val escape: output -> string
|
wenzelm@45296
|
24 |
val physical_stdout: output -> unit
|
wenzelm@45296
|
25 |
val physical_stderr: output -> unit
|
wenzelm@45296
|
26 |
val physical_writeln: output -> unit
|
wenzelm@40393
|
27 |
structure Private_Hooks:
|
wenzelm@40393
|
28 |
sig
|
wenzelm@40393
|
29 |
val writeln_fn: (output -> unit) Unsynchronized.ref
|
wenzelm@40393
|
30 |
val urgent_message_fn: (output -> unit) Unsynchronized.ref
|
wenzelm@40393
|
31 |
val tracing_fn: (output -> unit) Unsynchronized.ref
|
wenzelm@40393
|
32 |
val warning_fn: (output -> unit) Unsynchronized.ref
|
wenzelm@45153
|
33 |
val error_fn: (serial * output -> unit) Unsynchronized.ref
|
wenzelm@40393
|
34 |
val prompt_fn: (output -> unit) Unsynchronized.ref
|
wenzelm@40393
|
35 |
val status_fn: (output -> unit) Unsynchronized.ref
|
wenzelm@40393
|
36 |
val report_fn: (output -> unit) Unsynchronized.ref
|
wenzelm@51518
|
37 |
val result_fn: (serial * output -> unit) Unsynchronized.ref
|
wenzelm@47658
|
38 |
val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
|
wenzelm@40393
|
39 |
end
|
wenzelm@40392
|
40 |
val urgent_message: string -> unit
|
wenzelm@45153
|
41 |
val error_msg': serial * string -> unit
|
wenzelm@25845
|
42 |
val error_msg: string -> unit
|
wenzelm@25845
|
43 |
val prompt: string -> unit
|
wenzelm@27605
|
44 |
val status: string -> unit
|
wenzelm@38492
|
45 |
val report: string -> unit
|
wenzelm@51518
|
46 |
val result: serial * string -> unit
|
wenzelm@47658
|
47 |
val protocol_message: Properties.T -> string -> unit
|
wenzelm@50662
|
48 |
exception TRACING_LIMIT of int
|
wenzelm@14815
|
49 |
end;
|
wenzelm@14815
|
50 |
|
wenzelm@14815
|
51 |
structure Output: OUTPUT =
|
wenzelm@14815
|
52 |
struct
|
wenzelm@14815
|
53 |
|
wenzelm@23616
|
54 |
(** print modes **)
|
wenzelm@14881
|
55 |
|
wenzelm@23660
|
56 |
type output = string; (*raw system output*)
|
wenzelm@23660
|
57 |
|
wenzelm@23616
|
58 |
fun default_output s = (s, size s);
|
wenzelm@23660
|
59 |
fun default_escape (s: output) = s;
|
wenzelm@14955
|
60 |
|
wenzelm@23616
|
61 |
local
|
wenzelm@23616
|
62 |
val default = {output = default_output, escape = default_escape};
|
wenzelm@44563
|
63 |
val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
|
wenzelm@23616
|
64 |
in
|
wenzelm@44563
|
65 |
fun add_mode name output escape =
|
wenzelm@44563
|
66 |
Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
|
wenzelm@23616
|
67 |
fun get_mode () =
|
wenzelm@44563
|
68 |
the_default default
|
wenzelm@44563
|
69 |
(Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
|
wenzelm@23616
|
70 |
end;
|
wenzelm@14815
|
71 |
|
wenzelm@19265
|
72 |
fun output_width x = #output (get_mode ()) x;
|
wenzelm@14815
|
73 |
val output = #1 o output_width;
|
wenzelm@23727
|
74 |
|
wenzelm@23616
|
75 |
fun escape x = #escape (get_mode ()) x;
|
wenzelm@14815
|
76 |
|
wenzelm@14815
|
77 |
|
wenzelm@14815
|
78 |
|
wenzelm@14815
|
79 |
(** output channels **)
|
wenzelm@14815
|
80 |
|
wenzelm@40026
|
81 |
(* raw output primitives -- not to be used in user-space *)
|
wenzelm@14984
|
82 |
|
wenzelm@45296
|
83 |
fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
|
wenzelm@45296
|
84 |
fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
|
wenzelm@14815
|
85 |
|
wenzelm@45296
|
86 |
fun physical_writeln "" = ()
|
wenzelm@45296
|
87 |
| physical_writeln s = physical_stdout (suffix "\n" s); (*atomic output!*)
|
wenzelm@14815
|
88 |
|
wenzelm@14984
|
89 |
|
wenzelm@14984
|
90 |
(* Isabelle output channels *)
|
wenzelm@14984
|
91 |
|
wenzelm@40393
|
92 |
structure Private_Hooks =
|
wenzelm@40393
|
93 |
struct
|
wenzelm@45296
|
94 |
val writeln_fn = Unsynchronized.ref physical_writeln;
|
wenzelm@40393
|
95 |
val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
|
wenzelm@40393
|
96 |
val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
|
wenzelm@49014
|
97 |
val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
|
wenzelm@49014
|
98 |
val error_fn = Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
|
wenzelm@45296
|
99 |
val prompt_fn = Unsynchronized.ref physical_stdout;
|
wenzelm@44622
|
100 |
val status_fn = Unsynchronized.ref (fn _: output => ());
|
wenzelm@44622
|
101 |
val report_fn = Unsynchronized.ref (fn _: output => ());
|
wenzelm@51518
|
102 |
val result_fn = Unsynchronized.ref (fn _: serial * output => ());
|
wenzelm@47658
|
103 |
val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
|
wenzelm@47658
|
104 |
Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode");
|
wenzelm@40393
|
105 |
end;
|
wenzelm@14815
|
106 |
|
wenzelm@40393
|
107 |
fun writeln s = ! Private_Hooks.writeln_fn (output s);
|
wenzelm@40393
|
108 |
fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
|
wenzelm@40393
|
109 |
fun tracing s = ! Private_Hooks.tracing_fn (output s);
|
wenzelm@40393
|
110 |
fun warning s = ! Private_Hooks.warning_fn (output s);
|
wenzelm@45153
|
111 |
fun error_msg' (i, s) = ! Private_Hooks.error_fn (i, output s);
|
wenzelm@45153
|
112 |
fun error_msg s = error_msg' (serial (), s);
|
wenzelm@40393
|
113 |
fun prompt s = ! Private_Hooks.prompt_fn (output s);
|
wenzelm@40393
|
114 |
fun status s = ! Private_Hooks.status_fn (output s);
|
wenzelm@40393
|
115 |
fun report s = ! Private_Hooks.report_fn (output s);
|
wenzelm@51518
|
116 |
fun result (i, s) = ! Private_Hooks.result_fn (i, output s);
|
wenzelm@47658
|
117 |
fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
|
aspinall@15190
|
118 |
|
wenzelm@50662
|
119 |
exception TRACING_LIMIT of int;
|
wenzelm@50662
|
120 |
|
wenzelm@14815
|
121 |
end;
|
wenzelm@14815
|
122 |
|
wenzelm@32738
|
123 |
structure Basic_Output: BASIC_OUTPUT = Output;
|
wenzelm@32738
|
124 |
open Basic_Output;
|