src/Pure/General/output.ML
author wenzelm
Fri May 02 19:51:40 2014 +0200 (2014-05-02)
changeset 56830 e760242101fc
parent 56334 6b3739fee456
child 57975 c657c68a60ab
permissions -rw-r--r--
tuned signature -- channels for diagnostic output for system tools means stderr;
     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 prompt: string -> unit
    33   val status: string -> unit
    34   val report: string list -> unit
    35   val result: Properties.T -> string list -> unit
    36   val protocol_message: Properties.T -> string list -> unit
    37   val try_protocol_message: Properties.T -> string list -> unit
    38 end;
    39 
    40 signature PRIVATE_OUTPUT =
    41 sig
    42   include OUTPUT
    43   val writeln_fn: (output list -> unit) Unsynchronized.ref
    44   val urgent_message_fn: (output list -> unit) Unsynchronized.ref
    45   val tracing_fn: (output list -> unit) Unsynchronized.ref
    46   val warning_fn: (output list -> unit) Unsynchronized.ref
    47   val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
    48   val prompt_fn: (output -> unit) Unsynchronized.ref
    49   val status_fn: (output list -> unit) Unsynchronized.ref
    50   val report_fn: (output list -> unit) Unsynchronized.ref
    51   val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
    52   val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
    53 end;
    54 
    55 structure Output: PRIVATE_OUTPUT =
    56 struct
    57 
    58 (** print modes **)
    59 
    60 type output = string;  (*raw system output*)
    61 
    62 fun default_output s = (s, size s);
    63 fun default_escape (s: output) = s;
    64 
    65 local
    66   val default = {output = default_output, escape = default_escape};
    67   val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
    68 in
    69   fun add_mode name output escape =
    70     Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
    71   fun get_mode () =
    72     the_default default
    73       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
    74 end;
    75 
    76 fun output_width x = #output (get_mode ()) x;
    77 val output = #1 o output_width;
    78 
    79 fun escape x = #escape (get_mode ()) x;
    80 
    81 
    82 
    83 (** output channels **)
    84 
    85 (* raw output primitives -- not to be used in user-space *)
    86 
    87 fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    88 fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
    89 
    90 fun physical_writeln "" = ()
    91   | physical_writeln s = physical_stdout (suffix "\n" s);  (*atomic output!*)
    92 
    93 
    94 (* Isabelle output channels *)
    95 
    96 exception Protocol_Message of Properties.T;
    97 
    98 val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
    99 val urgent_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);  (*Proof General legacy*)
   100 val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
   101 val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
   102 val error_message_fn =
   103   Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
   104 val prompt_fn = Unsynchronized.ref physical_stdout;  (*Proof General legacy*)
   105 val status_fn = Unsynchronized.ref (fn _: output list => ());
   106 val report_fn = Unsynchronized.ref (fn _: output list => ());
   107 val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output list => ());
   108 val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref =
   109   Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
   110 
   111 fun writelns ss = ! writeln_fn (map output ss);
   112 fun writeln s = writelns [s];
   113 fun urgent_message s = ! urgent_message_fn [output s];  (*Proof General legacy*)
   114 fun tracing s = ! tracing_fn [output s];
   115 fun warning s = ! warning_fn [output s];
   116 fun error_message' (i, s) = ! error_message_fn (i, [output s]);
   117 fun error_message s = error_message' (serial (), s);
   118 fun prompt s = ! prompt_fn (output s);
   119 fun status s = ! status_fn [output s];
   120 fun report ss = ! report_fn (map output ss);
   121 fun result props ss = ! result_fn props (map output ss);
   122 fun protocol_message props ss = ! protocol_message_fn props (map output ss);
   123 fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
   124 
   125 end;
   126 
   127 structure Basic_Output: BASIC_OUTPUT = Output;
   128 open Basic_Output;