src/Pure/General/output.ML
author wenzelm
Fri Aug 15 13:39:59 2014 +0200 (2014-08-15)
changeset 57975 c657c68a60ab
parent 56830 e760242101fc
child 58843 521cea5fa777
permissions -rw-r--r--
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
more robust crash recovery: warning could crash again;
wenzelm@14815
     1
(*  Title:      Pure/General/output.ML
wenzelm@14815
     2
    Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
wenzelm@14815
     3
wenzelm@56830
     4
Isabelle channels for diagnostic output.
wenzelm@14815
     5
*)
wenzelm@14815
     6
wenzelm@14815
     7
signature BASIC_OUTPUT =
wenzelm@14815
     8
sig
wenzelm@18682
     9
  val writeln: string -> unit
wenzelm@18682
    10
  val tracing: string -> unit
wenzelm@18682
    11
  val warning: string -> unit
wenzelm@14815
    12
end;
wenzelm@14815
    13
wenzelm@14815
    14
signature OUTPUT =
wenzelm@14815
    15
sig
wenzelm@14815
    16
  include BASIC_OUTPUT
wenzelm@40131
    17
  type output = string
wenzelm@23660
    18
  val default_output: string -> output * int
wenzelm@23660
    19
  val default_escape: output -> string
wenzelm@23660
    20
  val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
wenzelm@23660
    21
  val output_width: string -> output * int
wenzelm@23660
    22
  val output: string -> output
wenzelm@23660
    23
  val escape: output -> string
wenzelm@44389
    24
  val physical_stdout: output -> unit
wenzelm@44389
    25
  val physical_stderr: output -> unit
wenzelm@44389
    26
  val physical_writeln: output -> unit
wenzelm@51661
    27
  exception Protocol_Message of Properties.T
wenzelm@56334
    28
  val writelns: string list -> unit
wenzelm@40132
    29
  val urgent_message: string -> unit
wenzelm@54387
    30
  val error_message': serial * string -> unit
wenzelm@54387
    31
  val error_message: string -> unit
wenzelm@57975
    32
  val system_message: string -> unit
wenzelm@25845
    33
  val prompt: string -> unit
wenzelm@27605
    34
  val status: string -> unit
wenzelm@56333
    35
  val report: string list -> unit
wenzelm@56333
    36
  val result: Properties.T -> string list -> unit
wenzelm@56333
    37
  val protocol_message: Properties.T -> string list -> unit
wenzelm@56333
    38
  val try_protocol_message: Properties.T -> string list -> unit
wenzelm@14815
    39
end;
wenzelm@14815
    40
wenzelm@55387
    41
signature PRIVATE_OUTPUT =
wenzelm@55387
    42
sig
wenzelm@55387
    43
  include OUTPUT
wenzelm@56333
    44
  val writeln_fn: (output list -> unit) Unsynchronized.ref
wenzelm@56333
    45
  val urgent_message_fn: (output list -> unit) Unsynchronized.ref
wenzelm@56333
    46
  val tracing_fn: (output list -> unit) Unsynchronized.ref
wenzelm@56333
    47
  val warning_fn: (output list -> unit) Unsynchronized.ref
wenzelm@56333
    48
  val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
wenzelm@57975
    49
  val system_message_fn: (output list -> unit) Unsynchronized.ref
wenzelm@55387
    50
  val prompt_fn: (output -> unit) Unsynchronized.ref
wenzelm@56333
    51
  val status_fn: (output list -> unit) Unsynchronized.ref
wenzelm@56333
    52
  val report_fn: (output list -> unit) Unsynchronized.ref
wenzelm@56333
    53
  val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
wenzelm@56333
    54
  val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
wenzelm@55387
    55
end;
wenzelm@55387
    56
wenzelm@55387
    57
structure Output: PRIVATE_OUTPUT =
wenzelm@14815
    58
struct
wenzelm@14815
    59
wenzelm@23616
    60
(** print modes **)
wenzelm@14881
    61
wenzelm@23660
    62
type output = string;  (*raw system output*)
wenzelm@23660
    63
wenzelm@23616
    64
fun default_output s = (s, size s);
wenzelm@23660
    65
fun default_escape (s: output) = s;
wenzelm@14815
    66
wenzelm@23616
    67
local
wenzelm@23616
    68
  val default = {output = default_output, escape = default_escape};
wenzelm@43684
    69
  val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
wenzelm@23616
    70
in
wenzelm@43684
    71
  fun add_mode name output escape =
wenzelm@43684
    72
    Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
wenzelm@23616
    73
  fun get_mode () =
wenzelm@43684
    74
    the_default default
wenzelm@43684
    75
      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
wenzelm@23616
    76
end;
wenzelm@14815
    77
wenzelm@19265
    78
fun output_width x = #output (get_mode ()) x;
wenzelm@14815
    79
val output = #1 o output_width;
wenzelm@23727
    80
wenzelm@23616
    81
fun escape x = #escape (get_mode ()) x;
wenzelm@14815
    82
wenzelm@14815
    83
wenzelm@14815
    84
wenzelm@14815
    85
(** output channels **)
wenzelm@14815
    86
wenzelm@39733
    87
(* raw output primitives -- not to be used in user-space *)
wenzelm@14984
    88
wenzelm@44389
    89
fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
wenzelm@44389
    90
fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
wenzelm@14815
    91
wenzelm@44389
    92
fun physical_writeln "" = ()
wenzelm@44389
    93
  | physical_writeln s = physical_stdout (suffix "\n" s);  (*atomic output!*)
wenzelm@14815
    94
wenzelm@14984
    95
wenzelm@14984
    96
(* Isabelle output channels *)
wenzelm@14984
    97
wenzelm@51661
    98
exception Protocol_Message of Properties.T;
wenzelm@51661
    99
wenzelm@56333
   100
val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
wenzelm@56333
   101
val urgent_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);  (*Proof General legacy*)
wenzelm@56333
   102
val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
wenzelm@56333
   103
val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
wenzelm@55387
   104
val error_message_fn =
wenzelm@56333
   105
  Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
wenzelm@57975
   106
val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
wenzelm@56333
   107
val prompt_fn = Unsynchronized.ref physical_stdout;  (*Proof General legacy*)
wenzelm@56333
   108
val status_fn = Unsynchronized.ref (fn _: output list => ());
wenzelm@56333
   109
val report_fn = Unsynchronized.ref (fn _: output list => ());
wenzelm@56333
   110
val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output list => ());
wenzelm@56333
   111
val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref =
wenzelm@55387
   112
  Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
wenzelm@14815
   113
wenzelm@56334
   114
fun writelns ss = ! writeln_fn (map output ss);
wenzelm@56334
   115
fun writeln s = writelns [s];
wenzelm@56333
   116
fun urgent_message s = ! urgent_message_fn [output s];  (*Proof General legacy*)
wenzelm@56333
   117
fun tracing s = ! tracing_fn [output s];
wenzelm@56333
   118
fun warning s = ! warning_fn [output s];
wenzelm@56333
   119
fun error_message' (i, s) = ! error_message_fn (i, [output s]);
wenzelm@54387
   120
fun error_message s = error_message' (serial (), s);
wenzelm@57975
   121
fun system_message s = ! system_message_fn [output s];
wenzelm@55387
   122
fun prompt s = ! prompt_fn (output s);
wenzelm@56333
   123
fun status s = ! status_fn [output s];
wenzelm@56333
   124
fun report ss = ! report_fn (map output ss);
wenzelm@56333
   125
fun result props ss = ! result_fn props (map output ss);
wenzelm@56333
   126
fun protocol_message props ss = ! protocol_message_fn props (map output ss);
wenzelm@56333
   127
fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
aspinall@15190
   128
wenzelm@14815
   129
end;
wenzelm@14815
   130
wenzelm@32738
   131
structure Basic_Output: BASIC_OUTPUT = Output;
wenzelm@32738
   132
open Basic_Output;