src/Pure/General/output.ML
author wenzelm
Sun, 27 Oct 2024 11:02:21 +0100 (2 months ago)
changeset 81266 8300511f4c45
parent 80849 e3a419073736
permissions -rw-r--r--
clarified signature;
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
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    13
end;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    14
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    15
signature OUTPUT =
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    16
sig
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    17
  include BASIC_OUTPUT
40131
7cbebd636e79 explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents: 40125
diff changeset
    18
  type output = string
44389
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 44270
diff changeset
    19
  val physical_stdout: output -> unit
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 44270
diff changeset
    20
  val physical_stderr: output -> unit
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 44270
diff changeset
    21
  val physical_writeln: output -> unit
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 70907
diff changeset
    22
  type protocol_message_fn = Output_Primitives.protocol_message_fn
51661
92e58b76dbb1 clarified protocol_message undefinedness;
wenzelm
parents: 50505
diff changeset
    23
  exception Protocol_Message of Properties.T
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 70907
diff changeset
    24
  val protocol_message_undefined: protocol_message_fn
56334
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 56333
diff changeset
    25
  val writelns: string list -> unit
59184
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 58850
diff changeset
    26
  val state: string -> unit
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 58850
diff changeset
    27
  val information: string -> unit
54387
890e983cb07b tuned signature;
wenzelm
parents: 53403
diff changeset
    28
  val error_message': serial * string -> unit
890e983cb07b tuned signature;
wenzelm
parents: 53403
diff changeset
    29
  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
    30
  val system_message: string -> unit
70662
0f9a4e8ee1ab tuned signature -- prefer bulk messages;
wenzelm
parents: 65301
diff changeset
    31
  val status: string list -> 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
    32
  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
    33
  val result: Properties.T -> string list -> unit
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 70907
diff changeset
    34
  val protocol_message: protocol_message_fn
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 70907
diff changeset
    35
  val try_protocol_message: protocol_message_fn
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    36
end;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    37
55387
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    38
signature PRIVATE_OUTPUT =
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    39
sig
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    40
  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
    41
  val writeln_fn: (output list -> unit) Unsynchronized.ref
59184
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 58850
diff changeset
    42
  val state_fn: (output list -> unit) Unsynchronized.ref
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 58850
diff changeset
    43
  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
    44
  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
    45
  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
    46
  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
    47
  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
    48
  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
    49
  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
    50
  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
    51
  val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 70907
diff changeset
    52
  val protocol_message_fn: Output_Primitives.protocol_message_fn Unsynchronized.ref
55387
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    53
end;
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    54
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    55
structure Private_Output: PRIVATE_OUTPUT =
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    56
struct
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    57
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    58
type output = string;  (*raw system output*)
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    59
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    60
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    61
(* primitives -- provided via bootstrap environment *)
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    62
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    63
val writeln_fn = Unsynchronized.ref Output_Primitives.writeln_fn;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    64
val state_fn = Unsynchronized.ref Output_Primitives.state_fn;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    65
val information_fn = Unsynchronized.ref Output_Primitives.information_fn;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    66
val tracing_fn = Unsynchronized.ref Output_Primitives.tracing_fn;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    67
val warning_fn = Unsynchronized.ref Output_Primitives.warning_fn;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    68
val legacy_fn = Unsynchronized.ref Output_Primitives.legacy_fn;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    69
val error_message_fn = Unsynchronized.ref Output_Primitives.error_message_fn;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    70
val system_message_fn = Unsynchronized.ref Output_Primitives.system_message_fn;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    71
val status_fn = Unsynchronized.ref Output_Primitives.status_fn;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    72
val report_fn = Unsynchronized.ref Output_Primitives.report_fn;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    73
val result_fn = Unsynchronized.ref Output_Primitives.result_fn;
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 70907
diff changeset
    74
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 70907
diff changeset
    75
type protocol_message_fn = Output_Primitives.protocol_message_fn;
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    76
val protocol_message_fn = Unsynchronized.ref Output_Primitives.protocol_message_fn;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    77
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    78
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
    79
(* physical output -- not to be used in user-space *)
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    80
44389
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 44270
diff changeset
    81
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
    82
fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    83
44389
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 44270
diff changeset
    84
fun physical_writeln "" = ()
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 44270
diff changeset
    85
  | physical_writeln s = physical_stdout (suffix "\n" s);  (*atomic output!*)
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    86
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    87
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    88
(* Isabelle output channels *)
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    89
51661
92e58b76dbb1 clarified protocol_message undefinedness;
wenzelm
parents: 50505
diff changeset
    90
exception Protocol_Message of Properties.T;
92e58b76dbb1 clarified protocol_message undefinedness;
wenzelm
parents: 50505
diff changeset
    91
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 70907
diff changeset
    92
val protocol_message_undefined: Output_Primitives.protocol_message_fn =
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 70907
diff changeset
    93
  fn props => fn _ => raise Protocol_Message props;
70907
7e3f25a0cee4 proper protocol_message for bootstrap proofs;
wenzelm
parents: 70662
diff changeset
    94
65301
fca593a62785 restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents: 63517
diff changeset
    95
fun init_channels () =
fca593a62785 restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents: 63517
diff changeset
    96
 (writeln_fn := (physical_writeln o implode);
fca593a62785 restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents: 63517
diff changeset
    97
  state_fn := (fn ss => ! writeln_fn ss);
fca593a62785 restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents: 63517
diff changeset
    98
  information_fn := Output_Primitives.ignore_outputs;
fca593a62785 restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents: 63517
diff changeset
    99
  tracing_fn := (fn ss => ! writeln_fn ss);
fca593a62785 restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents: 63517
diff changeset
   100
  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
   101
  legacy_fn := (fn ss => ! warning_fn ss);
fca593a62785 restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents: 63517
diff changeset
   102
  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
   103
  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
   104
  status_fn := Output_Primitives.ignore_outputs;
fca593a62785 restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents: 63517
diff changeset
   105
  report_fn := Output_Primitives.ignore_outputs;
fca593a62785 restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents: 63517
diff changeset
   106
  result_fn := (fn _ => Output_Primitives.ignore_outputs);
70907
7e3f25a0cee4 proper protocol_message for bootstrap proofs;
wenzelm
parents: 70662
diff changeset
   107
  protocol_message_fn := protocol_message_undefined);
65301
fca593a62785 restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents: 63517
diff changeset
   108
fca593a62785 restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents: 63517
diff changeset
   109
val _ = if Thread_Data.is_virtual then () else init_channels ();
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   110
80849
e3a419073736 drop pointless print_mode operations Output.output / Output.escape;
wenzelm
parents: 80846
diff changeset
   111
fun writelns ss = ! writeln_fn ss;
56334
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 56333
diff changeset
   112
fun writeln s = writelns [s];
80849
e3a419073736 drop pointless print_mode operations Output.output / Output.escape;
wenzelm
parents: 80846
diff changeset
   113
fun state s = ! state_fn [s];
e3a419073736 drop pointless print_mode operations Output.output / Output.escape;
wenzelm
parents: 80846
diff changeset
   114
fun information s = ! information_fn [s];
e3a419073736 drop pointless print_mode operations Output.output / Output.escape;
wenzelm
parents: 80846
diff changeset
   115
fun tracing s = ! tracing_fn [s];
e3a419073736 drop pointless print_mode operations Output.output / Output.escape;
wenzelm
parents: 80846
diff changeset
   116
fun warning s = ! warning_fn [s];
e3a419073736 drop pointless print_mode operations Output.output / Output.escape;
wenzelm
parents: 80846
diff changeset
   117
fun legacy_feature s = ! legacy_fn [("Legacy feature! " ^ s)];
e3a419073736 drop pointless print_mode operations Output.output / Output.escape;
wenzelm
parents: 80846
diff changeset
   118
fun error_message' (i, s) = ! error_message_fn (i, [s]);
54387
890e983cb07b tuned signature;
wenzelm
parents: 53403
diff changeset
   119
fun error_message s = error_message' (serial (), s);
80849
e3a419073736 drop pointless print_mode operations Output.output / Output.escape;
wenzelm
parents: 80846
diff changeset
   120
fun system_message s = ! system_message_fn [s];
e3a419073736 drop pointless print_mode operations Output.output / Output.escape;
wenzelm
parents: 80846
diff changeset
   121
fun status ss = ! status_fn ss;
e3a419073736 drop pointless print_mode operations Output.output / Output.escape;
wenzelm
parents: 80846
diff changeset
   122
fun report ss = ! report_fn ss;
e3a419073736 drop pointless print_mode operations Output.output / Output.escape;
wenzelm
parents: 80846
diff changeset
   123
fun result props ss = ! result_fn props ss;
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 70907
diff changeset
   124
fun protocol_message props body = ! protocol_message_fn props body;
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 70907
diff changeset
   125
fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => ();
15190
b6788dbd2ef9 Add info and debug output channels.
aspinall
parents: 15010
diff changeset
   126
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   127
end;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   128
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62894
diff changeset
   129
structure Output: OUTPUT = Private_Output;
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31685
diff changeset
   130
structure Basic_Output: BASIC_OUTPUT = Output;
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31685
diff changeset
   131
open Basic_Output;