src/Pure/General/output.ML
author wenzelm
Sat Apr 09 16:16:05 2016 +0200 (2016-04-09)
changeset 62930 51ac6bc389e8
parent 62894 047129a6e200
child 63517 8ea738cffabe
permissions -rw-r--r--
shared output primitives of physical/virtual Pure;
wenzelm@14815
     1
(*  Title:      Pure/General/output.ML
wenzelm@62930
     2
    Author:     Makarius
wenzelm@14815
     3
wenzelm@62930
     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@59203
    12
  val legacy_feature: string -> unit
wenzelm@61885
    13
  val profile_time: ('a -> 'b) -> 'a -> 'b
wenzelm@61885
    14
  val profile_time_thread: ('a -> 'b) -> 'a -> 'b
wenzelm@61885
    15
  val profile_allocations: ('a -> 'b) -> 'a -> 'b
wenzelm@14815
    16
end;
wenzelm@14815
    17
wenzelm@14815
    18
signature OUTPUT =
wenzelm@14815
    19
sig
wenzelm@14815
    20
  include BASIC_OUTPUT
wenzelm@40131
    21
  type output = string
wenzelm@23660
    22
  val default_output: string -> output * int
wenzelm@23660
    23
  val default_escape: output -> string
wenzelm@23660
    24
  val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
wenzelm@23660
    25
  val output_width: string -> output * int
wenzelm@23660
    26
  val output: string -> output
wenzelm@23660
    27
  val escape: output -> string
wenzelm@44389
    28
  val physical_stdout: output -> unit
wenzelm@44389
    29
  val physical_stderr: output -> unit
wenzelm@44389
    30
  val physical_writeln: output -> unit
wenzelm@51661
    31
  exception Protocol_Message of Properties.T
wenzelm@56334
    32
  val writelns: string list -> unit
wenzelm@59184
    33
  val state: string -> unit
wenzelm@59184
    34
  val information: string -> unit
wenzelm@54387
    35
  val error_message': serial * string -> unit
wenzelm@54387
    36
  val error_message: string -> unit
wenzelm@57975
    37
  val system_message: string -> unit
wenzelm@27605
    38
  val status: string -> unit
wenzelm@56333
    39
  val report: string list -> unit
wenzelm@56333
    40
  val result: Properties.T -> string list -> unit
wenzelm@56333
    41
  val protocol_message: Properties.T -> string list -> unit
wenzelm@56333
    42
  val try_protocol_message: Properties.T -> string list -> unit
wenzelm@14815
    43
end;
wenzelm@14815
    44
wenzelm@55387
    45
signature PRIVATE_OUTPUT =
wenzelm@55387
    46
sig
wenzelm@55387
    47
  include OUTPUT
wenzelm@56333
    48
  val writeln_fn: (output list -> unit) Unsynchronized.ref
wenzelm@59184
    49
  val state_fn: (output list -> unit) Unsynchronized.ref
wenzelm@59184
    50
  val information_fn: (output list -> unit) Unsynchronized.ref
wenzelm@56333
    51
  val tracing_fn: (output list -> unit) Unsynchronized.ref
wenzelm@56333
    52
  val warning_fn: (output list -> unit) Unsynchronized.ref
wenzelm@59203
    53
  val legacy_fn: (output list -> unit) Unsynchronized.ref
wenzelm@56333
    54
  val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
wenzelm@57975
    55
  val system_message_fn: (output list -> unit) Unsynchronized.ref
wenzelm@56333
    56
  val status_fn: (output list -> unit) Unsynchronized.ref
wenzelm@56333
    57
  val report_fn: (output list -> unit) Unsynchronized.ref
wenzelm@56333
    58
  val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
wenzelm@56333
    59
  val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
wenzelm@55387
    60
end;
wenzelm@55387
    61
wenzelm@62930
    62
structure Private_Output: PRIVATE_OUTPUT =
wenzelm@14815
    63
struct
wenzelm@14815
    64
wenzelm@23616
    65
(** print modes **)
wenzelm@14881
    66
wenzelm@23660
    67
type output = string;  (*raw system output*)
wenzelm@23660
    68
wenzelm@23616
    69
fun default_output s = (s, size s);
wenzelm@23660
    70
fun default_escape (s: output) = s;
wenzelm@14815
    71
wenzelm@23616
    72
local
wenzelm@23616
    73
  val default = {output = default_output, escape = default_escape};
wenzelm@43684
    74
  val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
wenzelm@23616
    75
in
wenzelm@43684
    76
  fun add_mode name output escape =
wenzelm@62894
    77
    if Thread_Data.is_virtual then ()
wenzelm@62894
    78
    else Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
wenzelm@23616
    79
  fun get_mode () =
wenzelm@43684
    80
    the_default default
wenzelm@43684
    81
      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
wenzelm@23616
    82
end;
wenzelm@14815
    83
wenzelm@19265
    84
fun output_width x = #output (get_mode ()) x;
wenzelm@14815
    85
val output = #1 o output_width;
wenzelm@23727
    86
wenzelm@23616
    87
fun escape x = #escape (get_mode ()) x;
wenzelm@14815
    88
wenzelm@14815
    89
wenzelm@14815
    90
wenzelm@14815
    91
(** output channels **)
wenzelm@14815
    92
wenzelm@62930
    93
(* primitives -- provided via bootstrap environment *)
wenzelm@62930
    94
wenzelm@62930
    95
val writeln_fn = Unsynchronized.ref Output_Primitives.writeln_fn;
wenzelm@62930
    96
val state_fn = Unsynchronized.ref Output_Primitives.state_fn;
wenzelm@62930
    97
val information_fn = Unsynchronized.ref Output_Primitives.information_fn;
wenzelm@62930
    98
val tracing_fn = Unsynchronized.ref Output_Primitives.tracing_fn;
wenzelm@62930
    99
val warning_fn = Unsynchronized.ref Output_Primitives.warning_fn;
wenzelm@62930
   100
val legacy_fn = Unsynchronized.ref Output_Primitives.legacy_fn;
wenzelm@62930
   101
val error_message_fn = Unsynchronized.ref Output_Primitives.error_message_fn;
wenzelm@62930
   102
val system_message_fn = Unsynchronized.ref Output_Primitives.system_message_fn;
wenzelm@62930
   103
val status_fn = Unsynchronized.ref Output_Primitives.status_fn;
wenzelm@62930
   104
val report_fn = Unsynchronized.ref Output_Primitives.report_fn;
wenzelm@62930
   105
val result_fn = Unsynchronized.ref Output_Primitives.result_fn;
wenzelm@62930
   106
val protocol_message_fn = Unsynchronized.ref Output_Primitives.protocol_message_fn;
wenzelm@62930
   107
wenzelm@62930
   108
wenzelm@62930
   109
(* physical output -- not to be used in user-space *)
wenzelm@14984
   110
wenzelm@44389
   111
fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
wenzelm@44389
   112
fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
wenzelm@14815
   113
wenzelm@44389
   114
fun physical_writeln "" = ()
wenzelm@44389
   115
  | physical_writeln s = physical_stdout (suffix "\n" s);  (*atomic output!*)
wenzelm@14815
   116
wenzelm@14984
   117
wenzelm@14984
   118
(* Isabelle output channels *)
wenzelm@14984
   119
wenzelm@51661
   120
exception Protocol_Message of Properties.T;
wenzelm@51661
   121
wenzelm@62930
   122
val _ =
wenzelm@62930
   123
  if Thread_Data.is_virtual then ()
wenzelm@62930
   124
  else
wenzelm@62930
   125
   (writeln_fn := (physical_writeln o implode);
wenzelm@62930
   126
    state_fn := (fn ss => ! writeln_fn ss);
wenzelm@62930
   127
    information_fn := (fn ss => ! writeln_fn ss);
wenzelm@62930
   128
    tracing_fn := (fn ss => ! writeln_fn ss);
wenzelm@62930
   129
    warning_fn := (physical_writeln o prefix_lines "### " o implode);
wenzelm@62930
   130
    legacy_fn := (fn ss => ! warning_fn ss);
wenzelm@62930
   131
    error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
wenzelm@62930
   132
    system_message_fn := (fn ss => ! writeln_fn ss);
wenzelm@62930
   133
    protocol_message_fn := (fn props => fn _ => raise Protocol_Message props));
wenzelm@14815
   134
wenzelm@56334
   135
fun writelns ss = ! writeln_fn (map output ss);
wenzelm@56334
   136
fun writeln s = writelns [s];
wenzelm@59184
   137
fun state s = ! state_fn [output s];
wenzelm@59184
   138
fun information s = ! information_fn [output s];
wenzelm@56333
   139
fun tracing s = ! tracing_fn [output s];
wenzelm@56333
   140
fun warning s = ! warning_fn [output s];
wenzelm@59203
   141
fun legacy_feature s = ! legacy_fn [output ("Legacy feature! " ^ s)];
wenzelm@56333
   142
fun error_message' (i, s) = ! error_message_fn (i, [output s]);
wenzelm@54387
   143
fun error_message s = error_message' (serial (), s);
wenzelm@57975
   144
fun system_message s = ! system_message_fn [output s];
wenzelm@56333
   145
fun status s = ! status_fn [output s];
wenzelm@56333
   146
fun report ss = ! report_fn (map output ss);
wenzelm@56333
   147
fun result props ss = ! result_fn props (map output ss);
wenzelm@56333
   148
fun protocol_message props ss = ! protocol_message_fn props (map output ss);
wenzelm@56333
   149
fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
aspinall@15190
   150
wenzelm@61885
   151
wenzelm@61885
   152
(* profiling *)
wenzelm@61885
   153
wenzelm@61885
   154
local
wenzelm@61885
   155
wenzelm@61885
   156
fun output_profile title entries =
wenzelm@61885
   157
  let
wenzelm@61885
   158
    val body = entries
wenzelm@61885
   159
      |> sort (int_ord o apply2 fst)
wenzelm@61885
   160
      |> map (fn (count, name) =>
wenzelm@61885
   161
          let
wenzelm@61885
   162
            val c = string_of_int count;
wenzelm@61885
   163
            val prefix = replicate_string (Int.max (0, 10 - size c)) " ";
wenzelm@61885
   164
          in prefix ^ c ^ " " ^ name end);
wenzelm@61885
   165
    val total = fold (curry (op +) o fst) entries 0;
wenzelm@61885
   166
  in
wenzelm@61885
   167
    if total = 0 then ()
wenzelm@61885
   168
    else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total])))
wenzelm@61885
   169
  end;
wenzelm@61885
   170
wenzelm@61885
   171
in
wenzelm@61885
   172
wenzelm@61885
   173
fun profile_time f x =
wenzelm@61885
   174
  ML_Profiling.profile_time (output_profile "time profile:") f x;
wenzelm@61885
   175
wenzelm@61885
   176
fun profile_time_thread f x =
wenzelm@61885
   177
  ML_Profiling.profile_time_thread (output_profile "time profile (this thread):") f x;
wenzelm@61885
   178
wenzelm@61885
   179
fun profile_allocations f x =
wenzelm@61885
   180
  ML_Profiling.profile_allocations (output_profile "allocations profile:") f x;
wenzelm@61885
   181
wenzelm@61885
   182
end;
wenzelm@61885
   183
wenzelm@61885
   184
wenzelm@14815
   185
end;
wenzelm@14815
   186
wenzelm@62930
   187
structure Output: OUTPUT = Private_Output;
wenzelm@32738
   188
structure Basic_Output: BASIC_OUTPUT = Output;
wenzelm@32738
   189
open Basic_Output;