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