src/Pure/General/output.ML
author wenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 45633 2cb7e34f6096
parent 44549 5e5e6ad3922c
child 46774 38f113b052b1
permissions -rw-r--r--
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm@14815
     1
(*  Title:      Pure/General/output.ML
wenzelm@14815
     2
    Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
wenzelm@14815
     3
wenzelm@42012
     4
Isabelle output channels.
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@40133
    27
  structure Private_Hooks:
wenzelm@40133
    28
  sig
wenzelm@40133
    29
    val writeln_fn: (output -> unit) Unsynchronized.ref
wenzelm@40133
    30
    val urgent_message_fn: (output -> unit) Unsynchronized.ref
wenzelm@40133
    31
    val tracing_fn: (output -> unit) Unsynchronized.ref
wenzelm@40133
    32
    val warning_fn: (output -> unit) Unsynchronized.ref
wenzelm@44270
    33
    val error_fn: (serial * output -> unit) Unsynchronized.ref
wenzelm@40133
    34
    val prompt_fn: (output -> unit) Unsynchronized.ref
wenzelm@40133
    35
    val status_fn: (output -> unit) Unsynchronized.ref
wenzelm@40133
    36
    val report_fn: (output -> unit) Unsynchronized.ref
wenzelm@43746
    37
    val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
wenzelm@40133
    38
  end
wenzelm@40132
    39
  val urgent_message: string -> unit
wenzelm@44270
    40
  val error_msg': serial * string -> unit
wenzelm@25845
    41
  val error_msg: string -> unit
wenzelm@25845
    42
  val prompt: string -> unit
wenzelm@27605
    43
  val status: string -> unit
wenzelm@38236
    44
  val report: string -> unit
wenzelm@43746
    45
  val raw_message: Properties.T -> string -> unit
wenzelm@14815
    46
end;
wenzelm@14815
    47
wenzelm@14815
    48
structure Output: OUTPUT =
wenzelm@14815
    49
struct
wenzelm@14815
    50
wenzelm@23616
    51
(** print modes **)
wenzelm@14881
    52
wenzelm@23660
    53
type output = string;  (*raw system output*)
wenzelm@23660
    54
wenzelm@23616
    55
fun default_output s = (s, size s);
wenzelm@23660
    56
fun default_escape (s: output) = s;
wenzelm@14815
    57
wenzelm@23616
    58
local
wenzelm@23616
    59
  val default = {output = default_output, escape = default_escape};
wenzelm@43684
    60
  val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
wenzelm@23616
    61
in
wenzelm@43684
    62
  fun add_mode name output escape =
wenzelm@43684
    63
    Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
wenzelm@23616
    64
  fun get_mode () =
wenzelm@43684
    65
    the_default default
wenzelm@43684
    66
      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
wenzelm@23616
    67
end;
wenzelm@14815
    68
wenzelm@19265
    69
fun output_width x = #output (get_mode ()) x;
wenzelm@14815
    70
val output = #1 o output_width;
wenzelm@23727
    71
wenzelm@23616
    72
fun escape x = #escape (get_mode ()) x;
wenzelm@14815
    73
wenzelm@14815
    74
wenzelm@14815
    75
wenzelm@14815
    76
(** output channels **)
wenzelm@14815
    77
wenzelm@39733
    78
(* raw output primitives -- not to be used in user-space *)
wenzelm@14984
    79
wenzelm@44389
    80
fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
wenzelm@44389
    81
fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
wenzelm@14815
    82
wenzelm@44389
    83
fun physical_writeln "" = ()
wenzelm@44389
    84
  | physical_writeln s = physical_stdout (suffix "\n" s);  (*atomic output!*)
wenzelm@14815
    85
wenzelm@14984
    86
wenzelm@14984
    87
(* Isabelle output channels *)
wenzelm@14984
    88
wenzelm@40133
    89
structure Private_Hooks =
wenzelm@40133
    90
struct
wenzelm@44389
    91
  val writeln_fn = Unsynchronized.ref physical_writeln;
wenzelm@40133
    92
  val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
wenzelm@40133
    93
  val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
wenzelm@44389
    94
  val warning_fn = Unsynchronized.ref (physical_stdout o suffix "\n" o prefix_lines "### ");
wenzelm@44270
    95
  val error_fn =
wenzelm@44389
    96
    Unsynchronized.ref (fn (_: serial, s) => physical_stdout (suffix "\n" (prefix_lines "*** " s)));
wenzelm@44389
    97
  val prompt_fn = Unsynchronized.ref physical_stdout;
wenzelm@43746
    98
  val status_fn = Unsynchronized.ref (fn _: output => ());
wenzelm@43746
    99
  val report_fn = Unsynchronized.ref (fn _: output => ());
wenzelm@43760
   100
  val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
wenzelm@43760
   101
    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.raw_message undefined in TTY mode");
wenzelm@40133
   102
end;
wenzelm@14815
   103
wenzelm@40133
   104
fun writeln s = ! Private_Hooks.writeln_fn (output s);
wenzelm@40133
   105
fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
wenzelm@40133
   106
fun tracing s = ! Private_Hooks.tracing_fn (output s);
wenzelm@40133
   107
fun warning s = ! Private_Hooks.warning_fn (output s);
wenzelm@44270
   108
fun error_msg' (i, s) = ! Private_Hooks.error_fn (i, output s);
wenzelm@44270
   109
fun error_msg s = error_msg' (serial (), s);
wenzelm@40133
   110
fun prompt s = ! Private_Hooks.prompt_fn (output s);
wenzelm@40133
   111
fun status s = ! Private_Hooks.status_fn (output s);
wenzelm@40133
   112
fun report s = ! Private_Hooks.report_fn (output s);
wenzelm@43746
   113
fun raw_message props s = ! Private_Hooks.raw_message_fn props (output s);
aspinall@15190
   114
wenzelm@14815
   115
end;
wenzelm@14815
   116
wenzelm@32738
   117
structure Basic_Output: BASIC_OUTPUT = Output;
wenzelm@32738
   118
open Basic_Output;