author | wenzelm |
Mon, 25 Mar 2019 16:45:08 +0100 | |
changeset 69980 | f2e3adfd916f |
parent 65301 | fca593a62785 |
child 70662 | 0f9a4e8ee1ab |
permissions | -rw-r--r-- |
14815 | 1 |
(* Title: Pure/General/output.ML |
62930
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
2 |
Author: Makarius |
14815 | 3 |
|
62930
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
4 |
Isabelle output channels. |
14815 | 5 |
*) |
6 |
||
7 |
signature BASIC_OUTPUT = |
|
8 |
sig |
|
18682
216692feebab
removed special ERROR handling stuff (transform_error etc.);
wenzelm
parents:
17539
diff
changeset
|
9 |
val writeln: string -> unit |
216692feebab
removed special ERROR handling stuff (transform_error etc.);
wenzelm
parents:
17539
diff
changeset
|
10 |
val tracing: string -> unit |
216692feebab
removed special ERROR handling stuff (transform_error etc.);
wenzelm
parents:
17539
diff
changeset
|
11 |
val warning: string -> unit |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
12 |
val legacy_feature: string -> unit |
61885
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
13 |
val profile_time: ('a -> 'b) -> 'a -> 'b |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
14 |
val profile_time_thread: ('a -> 'b) -> 'a -> 'b |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
15 |
val profile_allocations: ('a -> 'b) -> 'a -> 'b |
14815 | 16 |
end; |
17 |
||
18 |
signature OUTPUT = |
|
19 |
sig |
|
20 |
include BASIC_OUTPUT |
|
40131
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
40125
diff
changeset
|
21 |
type output = string |
23660
18765718cf62
type output = string indicates raw system output;
wenzelm
parents:
23616
diff
changeset
|
22 |
val default_output: string -> output * int |
18765718cf62
type output = string indicates raw system output;
wenzelm
parents:
23616
diff
changeset
|
23 |
val default_escape: output -> string |
18765718cf62
type output = string indicates raw system output;
wenzelm
parents:
23616
diff
changeset
|
24 |
val add_mode: string -> (string -> output * int) -> (output -> string) -> unit |
18765718cf62
type output = string indicates raw system output;
wenzelm
parents:
23616
diff
changeset
|
25 |
val output_width: string -> output * int |
18765718cf62
type output = string indicates raw system output;
wenzelm
parents:
23616
diff
changeset
|
26 |
val output: string -> output |
18765718cf62
type output = string indicates raw system output;
wenzelm
parents:
23616
diff
changeset
|
27 |
val escape: output -> string |
44389
a3b5fdfb04a3
tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents:
44270
diff
changeset
|
28 |
val physical_stdout: output -> unit |
a3b5fdfb04a3
tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents:
44270
diff
changeset
|
29 |
val physical_stderr: output -> unit |
a3b5fdfb04a3
tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents:
44270
diff
changeset
|
30 |
val physical_writeln: output -> unit |
51661 | 31 |
exception Protocol_Message of Properties.T |
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56333
diff
changeset
|
32 |
val writelns: string list -> unit |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
58850
diff
changeset
|
33 |
val state: string -> unit |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
58850
diff
changeset
|
34 |
val information: string -> unit |
54387 | 35 |
val error_message': serial * string -> unit |
36 |
val error_message: string -> unit |
|
57975
c657c68a60ab
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
wenzelm
parents:
56830
diff
changeset
|
37 |
val system_message: string -> unit |
27605 | 38 |
val status: string -> unit |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
39 |
val report: string list -> unit |
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
40 |
val result: Properties.T -> string list -> unit |
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
41 |
val protocol_message: Properties.T -> string list -> unit |
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
42 |
val try_protocol_message: Properties.T -> string list -> unit |
14815 | 43 |
end; |
44 |
||
55387
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54387
diff
changeset
|
45 |
signature PRIVATE_OUTPUT = |
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54387
diff
changeset
|
46 |
sig |
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54387
diff
changeset
|
47 |
include OUTPUT |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
48 |
val writeln_fn: (output list -> unit) Unsynchronized.ref |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
58850
diff
changeset
|
49 |
val state_fn: (output list -> unit) Unsynchronized.ref |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
58850
diff
changeset
|
50 |
val information_fn: (output list -> unit) Unsynchronized.ref |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
51 |
val tracing_fn: (output list -> unit) Unsynchronized.ref |
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
52 |
val warning_fn: (output list -> unit) Unsynchronized.ref |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
53 |
val legacy_fn: (output list -> unit) Unsynchronized.ref |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
54 |
val error_message_fn: (serial * output list -> unit) Unsynchronized.ref |
57975
c657c68a60ab
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
wenzelm
parents:
56830
diff
changeset
|
55 |
val system_message_fn: (output list -> unit) Unsynchronized.ref |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
56 |
val status_fn: (output list -> unit) Unsynchronized.ref |
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
57 |
val report_fn: (output list -> unit) Unsynchronized.ref |
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
58 |
val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref |
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
59 |
val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref |
65301
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
60 |
val init_channels: unit -> unit |
55387
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54387
diff
changeset
|
61 |
end; |
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54387
diff
changeset
|
62 |
|
62930
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
63 |
structure Private_Output: PRIVATE_OUTPUT = |
14815 | 64 |
struct |
65 |
||
23616 | 66 |
(** print modes **) |
14881 | 67 |
|
23660
18765718cf62
type output = string indicates raw system output;
wenzelm
parents:
23616
diff
changeset
|
68 |
type output = string; (*raw system output*) |
18765718cf62
type output = string indicates raw system output;
wenzelm
parents:
23616
diff
changeset
|
69 |
|
23616 | 70 |
fun default_output s = (s, size s); |
23660
18765718cf62
type output = string indicates raw system output;
wenzelm
parents:
23616
diff
changeset
|
71 |
fun default_escape (s: output) = s; |
14815 | 72 |
|
23616 | 73 |
local |
74 |
val default = {output = default_output, escape = default_escape}; |
|
43684 | 75 |
val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]); |
23616 | 76 |
in |
43684 | 77 |
fun add_mode name output escape = |
62894 | 78 |
if Thread_Data.is_virtual then () |
79 |
else Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})); |
|
23616 | 80 |
fun get_mode () = |
43684 | 81 |
the_default default |
82 |
(Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); |
|
23616 | 83 |
end; |
14815 | 84 |
|
19265 | 85 |
fun output_width x = #output (get_mode ()) x; |
14815 | 86 |
val output = #1 o output_width; |
23727 | 87 |
|
23616 | 88 |
fun escape x = #escape (get_mode ()) x; |
14815 | 89 |
|
90 |
||
91 |
||
92 |
(** output channels **) |
|
93 |
||
62930
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
94 |
(* primitives -- provided via bootstrap environment *) |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
95 |
|
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
96 |
val writeln_fn = Unsynchronized.ref Output_Primitives.writeln_fn; |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
97 |
val state_fn = Unsynchronized.ref Output_Primitives.state_fn; |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
98 |
val information_fn = Unsynchronized.ref Output_Primitives.information_fn; |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
99 |
val tracing_fn = Unsynchronized.ref Output_Primitives.tracing_fn; |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
100 |
val warning_fn = Unsynchronized.ref Output_Primitives.warning_fn; |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
101 |
val legacy_fn = Unsynchronized.ref Output_Primitives.legacy_fn; |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
102 |
val error_message_fn = Unsynchronized.ref Output_Primitives.error_message_fn; |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
103 |
val system_message_fn = Unsynchronized.ref Output_Primitives.system_message_fn; |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
104 |
val status_fn = Unsynchronized.ref Output_Primitives.status_fn; |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
105 |
val report_fn = Unsynchronized.ref Output_Primitives.report_fn; |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
106 |
val result_fn = Unsynchronized.ref Output_Primitives.result_fn; |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
107 |
val protocol_message_fn = Unsynchronized.ref Output_Primitives.protocol_message_fn; |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
108 |
|
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
109 |
|
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
110 |
(* physical output -- not to be used in user-space *) |
14984 | 111 |
|
44389
a3b5fdfb04a3
tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents:
44270
diff
changeset
|
112 |
fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); |
a3b5fdfb04a3
tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents:
44270
diff
changeset
|
113 |
fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr); |
14815 | 114 |
|
44389
a3b5fdfb04a3
tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents:
44270
diff
changeset
|
115 |
fun physical_writeln "" = () |
a3b5fdfb04a3
tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents:
44270
diff
changeset
|
116 |
| physical_writeln s = physical_stdout (suffix "\n" s); (*atomic output!*) |
14815 | 117 |
|
14984 | 118 |
|
119 |
(* Isabelle output channels *) |
|
120 |
||
51661 | 121 |
exception Protocol_Message of Properties.T; |
122 |
||
65301
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
123 |
fun init_channels () = |
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
124 |
(writeln_fn := (physical_writeln o implode); |
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
125 |
state_fn := (fn ss => ! writeln_fn ss); |
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
126 |
information_fn := Output_Primitives.ignore_outputs; |
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
127 |
tracing_fn := (fn ss => ! writeln_fn ss); |
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
128 |
warning_fn := (physical_writeln o prefix_lines "### " o implode); |
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
129 |
legacy_fn := (fn ss => ! warning_fn ss); |
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
130 |
error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss))); |
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
131 |
system_message_fn := (fn ss => ! writeln_fn ss); |
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
132 |
status_fn := Output_Primitives.ignore_outputs; |
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
133 |
report_fn := Output_Primitives.ignore_outputs; |
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
134 |
result_fn := (fn _ => Output_Primitives.ignore_outputs); |
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
135 |
protocol_message_fn := (fn props => fn _ => raise Protocol_Message props)); |
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
136 |
|
fca593a62785
restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents:
63517
diff
changeset
|
137 |
val _ = if Thread_Data.is_virtual then () else init_channels (); |
14815 | 138 |
|
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56333
diff
changeset
|
139 |
fun writelns ss = ! writeln_fn (map output ss); |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56333
diff
changeset
|
140 |
fun writeln s = writelns [s]; |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
58850
diff
changeset
|
141 |
fun state s = ! state_fn [output s]; |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
58850
diff
changeset
|
142 |
fun information s = ! information_fn [output s]; |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
143 |
fun tracing s = ! tracing_fn [output s]; |
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
144 |
fun warning s = ! warning_fn [output s]; |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
145 |
fun legacy_feature s = ! legacy_fn [output ("Legacy feature! " ^ s)]; |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
146 |
fun error_message' (i, s) = ! error_message_fn (i, [output s]); |
54387 | 147 |
fun error_message s = error_message' (serial (), s); |
57975
c657c68a60ab
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
wenzelm
parents:
56830
diff
changeset
|
148 |
fun system_message s = ! system_message_fn [output s]; |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
149 |
fun status s = ! status_fn [output s]; |
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
150 |
fun report ss = ! report_fn (map output ss); |
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
151 |
fun result props ss = ! result_fn props (map output ss); |
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
152 |
fun protocol_message props ss = ! protocol_message_fn props (map output ss); |
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56304
diff
changeset
|
153 |
fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => (); |
15190 | 154 |
|
61885
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
155 |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
156 |
(* profiling *) |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
157 |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
158 |
local |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
159 |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
160 |
fun output_profile title entries = |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
161 |
let |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
162 |
val body = entries |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
163 |
|> sort (int_ord o apply2 fst) |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
164 |
|> map (fn (count, name) => |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
165 |
let |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
166 |
val c = string_of_int count; |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
167 |
val prefix = replicate_string (Int.max (0, 10 - size c)) " "; |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
168 |
in prefix ^ c ^ " " ^ name end); |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
169 |
val total = fold (curry (op +) o fst) entries 0; |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
170 |
in |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
171 |
if total = 0 then () |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
172 |
else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total]))) |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
173 |
end; |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
174 |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
175 |
in |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
176 |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
177 |
fun profile_time f x = |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
178 |
ML_Profiling.profile_time (output_profile "time profile:") f x; |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
179 |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
180 |
fun profile_time_thread f x = |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
181 |
ML_Profiling.profile_time_thread (output_profile "time profile (this thread):") f x; |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
182 |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
183 |
fun profile_allocations f x = |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
184 |
ML_Profiling.profile_allocations (output_profile "allocations profile:") f x; |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
185 |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
186 |
end; |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
187 |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
59203
diff
changeset
|
188 |
|
14815 | 189 |
end; |
190 |
||
62930
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62894
diff
changeset
|
191 |
structure Output: OUTPUT = Private_Output; |
32738 | 192 |
structure Basic_Output: BASIC_OUTPUT = Output; |
193 |
open Basic_Output; |