src/Pure/General/output.ML
author wenzelm
Sat, 18 Mar 2017 12:46:52 +0100
changeset 65301 fca593a62785
parent 63517 8ea738cffabe
child 70662 0f9a4e8ee1ab
permissions -rw-r--r--
restore output channels after shutdown, e.g. relevant for saved heap;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/output.ML
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
     2
    Author:     Makarius
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     3
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
     4
Isabelle output channels.
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     5
*)
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     6
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     7
signature BASIC_OUTPUT =
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     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
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    16
end;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    17
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    18
signature OUTPUT =
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    19
sig
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    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
92e58b76dbb1 clarified protocol_message undefinedness;
wenzelm
parents: 50505
diff changeset
    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
890e983cb07b tuned signature;
wenzelm
parents: 53403
diff changeset
    35
  val error_message': serial * string -> unit
890e983cb07b tuned signature;
wenzelm
parents: 53403
diff changeset
    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
2c281958e45d added status channel;
wenzelm
parents: 26291
diff changeset
    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
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    43
end;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    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
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    64
struct
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    65
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    66
(** print modes **)
14881
e1f501a14159 added has_mode; handle_error: output raw;
wenzelm
parents: 14869
diff changeset
    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
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    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
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    72
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    73
local
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    74
  val default = {output = default_output, escape = default_escape};
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42012
diff changeset
    75
  val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    76
in
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42012
diff changeset
    77
  fun add_mode name output escape =
62894
047129a6e200 more robust bootstrap;
wenzelm
parents: 61885
diff changeset
    78
    if Thread_Data.is_virtual then ()
047129a6e200 more robust bootstrap;
wenzelm
parents: 61885
diff changeset
    79
    else Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    80
  fun get_mode () =
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42012
diff changeset
    81
    the_default default
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42012
diff changeset
    82
      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    83
end;
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    84
19265
cae36e16f3c0 Output.add_mode: keyword component;
wenzelm
parents: 18716
diff changeset
    85
fun output_width x = #output (get_mode ()) x;
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    86
val output = #1 o output_width;
23727
39f8d1480d55 added escape_malformed (failsafe);
wenzelm
parents: 23660
diff changeset
    87
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    88
fun escape x = #escape (get_mode ()) x;
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    89
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    90
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    91
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    92
(** output channels **)
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    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
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
   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
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   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
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   117
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
   118
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
   119
(* Isabelle output channels *)
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
   120
51661
92e58b76dbb1 clarified protocol_message undefinedness;
wenzelm
parents: 50505
diff changeset
   121
exception Protocol_Message of Properties.T;
92e58b76dbb1 clarified protocol_message undefinedness;
wenzelm
parents: 50505
diff changeset
   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
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   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
890e983cb07b tuned signature;
wenzelm
parents: 53403
diff changeset
   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
b6788dbd2ef9 Add info and debug output channels.
aspinall
parents: 15010
diff changeset
   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
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   189
end;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   190
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
   191
structure Output: OUTPUT = Private_Output;
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31685
diff changeset
   192
structure Basic_Output: BASIC_OUTPUT = Output;
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31685
diff changeset
   193
open Basic_Output;