src/Pure/General/output.ML
author wenzelm
Wed, 26 Mar 2014 20:32:15 +0100
changeset 56297 3925634718fb
parent 55387 51f0876f61df
child 56304 40274e4f5ebf
permissions -rw-r--r--
support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/output.ML
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     3
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40133
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
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    12
end;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    13
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    14
signature OUTPUT =
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    15
sig
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    16
  include BASIC_OUTPUT
40131
7cbebd636e79 explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents: 40125
diff changeset
    17
  type output = string
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    18
  val default_output: string -> output * int
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    19
  val default_escape: output -> string
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    20
  val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    21
  val output_width: string -> output * int
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    22
  val output: string -> output
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    23
  val escape: output -> string
44389
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 44270
diff changeset
    24
  val physical_stdout: output -> unit
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 44270
diff changeset
    25
  val physical_stderr: output -> unit
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 44270
diff changeset
    26
  val physical_writeln: output -> unit
51661
92e58b76dbb1 clarified protocol_message undefinedness;
wenzelm
parents: 50505
diff changeset
    27
  exception Protocol_Message of Properties.T
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 40131
diff changeset
    28
  val urgent_message: string -> unit
54387
890e983cb07b tuned signature;
wenzelm
parents: 53403
diff changeset
    29
  val error_message': serial * string -> unit
890e983cb07b tuned signature;
wenzelm
parents: 53403
diff changeset
    30
  val error_message: string -> unit
25845
c448a5f15f31 added explicit prompt channel (prompt_fn/prompt);
wenzelm
parents: 25686
diff changeset
    31
  val prompt: string -> unit
27605
2c281958e45d added status channel;
wenzelm
parents: 26291
diff changeset
    32
  val status: string -> unit
56297
3925634718fb support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm
parents: 55387
diff changeset
    33
  val direct_report: string -> unit
3925634718fb support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm
parents: 55387
diff changeset
    34
  val redirect_report: (string -> unit) -> ('a -> 'b) -> 'a -> 'b
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 37784
diff changeset
    35
  val report: string -> unit
52854
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52852
diff changeset
    36
  val result: Properties.T -> string -> unit
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 44549
diff changeset
    37
  val protocol_message: Properties.T -> string -> unit
51661
92e58b76dbb1 clarified protocol_message undefinedness;
wenzelm
parents: 50505
diff changeset
    38
  val try_protocol_message: Properties.T -> string -> unit
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    39
end;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    40
55387
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    41
signature PRIVATE_OUTPUT =
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    42
sig
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    43
  include OUTPUT
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    44
  val writeln_fn: (output -> unit) Unsynchronized.ref
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    45
  val urgent_message_fn: (output -> unit) Unsynchronized.ref
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    46
  val tracing_fn: (output -> unit) Unsynchronized.ref
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    47
  val warning_fn: (output -> unit) Unsynchronized.ref
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    48
  val error_message_fn: (serial * output -> unit) Unsynchronized.ref
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    49
  val prompt_fn: (output -> unit) Unsynchronized.ref
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    50
  val status_fn: (output -> unit) Unsynchronized.ref
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    51
  val report_fn: (output -> unit) Unsynchronized.ref
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    52
  val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    53
  val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    54
end;
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    55
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    56
structure Output: PRIVATE_OUTPUT =
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    57
struct
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    58
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    59
(** print modes **)
14881
e1f501a14159 added has_mode; handle_error: output raw;
wenzelm
parents: 14869
diff changeset
    60
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    61
type output = string;  (*raw system output*)
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    62
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    63
fun default_output s = (s, size s);
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    64
fun default_escape (s: output) = s;
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    65
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    66
local
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    67
  val default = {output = default_output, escape = default_escape};
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42012
diff changeset
    68
  val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    69
in
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42012
diff changeset
    70
  fun add_mode name output escape =
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42012
diff changeset
    71
    Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    72
  fun get_mode () =
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42012
diff changeset
    73
    the_default default
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42012
diff changeset
    74
      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    75
end;
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    76
19265
cae36e16f3c0 Output.add_mode: keyword component;
wenzelm
parents: 18716
diff changeset
    77
fun output_width x = #output (get_mode ()) x;
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    78
val output = #1 o output_width;
23727
39f8d1480d55 added escape_malformed (failsafe);
wenzelm
parents: 23660
diff changeset
    79
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    80
fun escape x = #escape (get_mode ()) x;
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    81
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    82
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    83
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    84
(** output channels **)
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    85
39733
6d373e9dcb9d renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
wenzelm
parents: 38839
diff changeset
    86
(* raw output primitives -- not to be used in user-space *)
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    87
44389
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 44270
diff changeset
    88
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
    89
fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    90
44389
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 44270
diff changeset
    91
fun physical_writeln "" = ()
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 44270
diff changeset
    92
  | physical_writeln s = physical_stdout (suffix "\n" s);  (*atomic output!*)
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    93
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    94
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    95
(* Isabelle output channels *)
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    96
51661
92e58b76dbb1 clarified protocol_message undefinedness;
wenzelm
parents: 50505
diff changeset
    97
exception Protocol_Message of Properties.T;
92e58b76dbb1 clarified protocol_message undefinedness;
wenzelm
parents: 50505
diff changeset
    98
55387
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
    99
val writeln_fn = Unsynchronized.ref physical_writeln;
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   100
val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);  (*Proof General legacy*)
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   101
val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   102
val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   103
val error_message_fn =
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   104
  Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   105
val prompt_fn = Unsynchronized.ref physical_stdout;
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   106
val status_fn = Unsynchronized.ref (fn _: output => ());
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   107
val report_fn = Unsynchronized.ref (fn _: output => ());
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   108
val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   109
val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   110
  Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   111
55387
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   112
fun writeln s = ! writeln_fn (output s);
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   113
fun urgent_message s = ! urgent_message_fn (output s);  (*Proof General legacy*)
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   114
fun tracing s = ! tracing_fn (output s);
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   115
fun warning s = ! warning_fn (output s);
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   116
fun error_message' (i, s) = ! error_message_fn (i, output s);
54387
890e983cb07b tuned signature;
wenzelm
parents: 53403
diff changeset
   117
fun error_message s = error_message' (serial (), s);
55387
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   118
fun prompt s = ! prompt_fn (output s);
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   119
fun status s = ! status_fn (output s);
56297
3925634718fb support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm
parents: 55387
diff changeset
   120
3925634718fb support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm
parents: 55387
diff changeset
   121
fun direct_report s = ! report_fn (output s);
3925634718fb support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm
parents: 55387
diff changeset
   122
3925634718fb support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm
parents: 55387
diff changeset
   123
local
3925634718fb support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm
parents: 55387
diff changeset
   124
  val tag = Universal.tag () : (string -> unit) Universal.tag;
3925634718fb support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm
parents: 55387
diff changeset
   125
  fun thread_data () = the_default direct_report (Thread.getLocal tag);
3925634718fb support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm
parents: 55387
diff changeset
   126
in
3925634718fb support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm
parents: 55387
diff changeset
   127
  fun redirect_report rep = Library.setmp_thread_data tag (thread_data ()) rep;
3925634718fb support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm
parents: 55387
diff changeset
   128
  fun report s = thread_data () s;
3925634718fb support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm
parents: 55387
diff changeset
   129
end;
3925634718fb support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
wenzelm
parents: 55387
diff changeset
   130
55387
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   131
fun result props s = ! result_fn props (output s);
51f0876f61df seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents: 54387
diff changeset
   132
fun protocol_message props s = ! protocol_message_fn props (output s);
51661
92e58b76dbb1 clarified protocol_message undefinedness;
wenzelm
parents: 50505
diff changeset
   133
fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
15190
b6788dbd2ef9 Add info and debug output channels.
aspinall
parents: 15010
diff changeset
   134
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   135
end;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   136
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31685
diff changeset
   137
structure Basic_Output: BASIC_OUTPUT = Output;
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31685
diff changeset
   138
open Basic_Output;