src/Pure/General/output.ML
author wenzelm
Thu Jul 19 23:18:46 2007 +0200 (2007-07-19)
changeset 23862 b1861768d8f4
parent 23727 39f8d1480d55
child 23922 707639e9497d
permissions -rw-r--r--
tuned;
wenzelm@14815
     1
(*  Title:      Pure/General/output.ML
wenzelm@14815
     2
    ID:         $Id$
wenzelm@14815
     3
    Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
wenzelm@14815
     4
wenzelm@22585
     5
Output channels and timing messages.
wenzelm@14815
     6
*)
wenzelm@14815
     7
wenzelm@14815
     8
signature BASIC_OUTPUT =
wenzelm@14815
     9
sig
wenzelm@23660
    10
  type output = string
wenzelm@18682
    11
  val writeln: string -> unit
wenzelm@18682
    12
  val priority: string -> unit
wenzelm@18682
    13
  val tracing: string -> unit
wenzelm@18682
    14
  val warning: string -> unit
wenzelm@22826
    15
  val tolerate_legacy_features: bool ref
wenzelm@22826
    16
  val legacy_feature: string -> unit
wenzelm@14869
    17
  val timing: bool ref
wenzelm@14815
    18
  val cond_timeit: bool -> (unit -> 'a) -> 'a
wenzelm@14815
    19
  val timeit: (unit -> 'a) -> 'a
wenzelm@14815
    20
  val timeap: ('a -> 'b) -> 'a -> 'b
wenzelm@14815
    21
  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
wenzelm@16726
    22
  val time_accumulator: string -> ('a -> 'b) -> 'a -> 'b
wenzelm@14815
    23
end;
wenzelm@14815
    24
wenzelm@14815
    25
signature OUTPUT =
wenzelm@14815
    26
sig
wenzelm@14815
    27
  include BASIC_OUTPUT
wenzelm@23660
    28
  val default_output: string -> output * int
wenzelm@23660
    29
  val default_escape: output -> string
wenzelm@23660
    30
  val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
wenzelm@23660
    31
  val output_width: string -> output * int
wenzelm@23660
    32
  val output: string -> output
wenzelm@23660
    33
  val escape: output -> string
wenzelm@23727
    34
  val escape_malformed: string -> string
wenzelm@23660
    35
  val std_output: output -> unit
wenzelm@23660
    36
  val std_error: output -> unit
wenzelm@22585
    37
  val immediate_output: string -> unit
wenzelm@23660
    38
  val writeln_default: output -> unit
wenzelm@23660
    39
  val writeln_fn: (output -> unit) ref
wenzelm@23660
    40
  val priority_fn: (output -> unit) ref
wenzelm@23660
    41
  val tracing_fn: (output -> unit) ref
wenzelm@23660
    42
  val warning_fn: (output -> unit) ref
wenzelm@23660
    43
  val error_fn: (output -> unit) ref
wenzelm@23660
    44
  val debug_fn: (output -> unit) ref
wenzelm@22585
    45
  val debugging: bool ref
wenzelm@22585
    46
  val no_warnings: ('a -> 'b) -> 'a -> 'b
wenzelm@18682
    47
  exception TOPLEVEL_ERROR
wenzelm@18682
    48
  val do_toplevel_errors: bool ref
wenzelm@18682
    49
  val toplevel_errors: ('a -> 'b) -> 'a -> 'b
wenzelm@18716
    50
  val ML_errors: ('a -> 'b) -> 'a -> 'b
wenzelm@22130
    51
  val debug: (unit -> string) -> unit
wenzelm@18682
    52
  val error_msg: string -> unit
wenzelm@20926
    53
  val ml_output: (string -> unit) * (string -> unit)
wenzelm@16726
    54
  val accumulated_time: unit -> unit
wenzelm@14815
    55
end;
wenzelm@14815
    56
wenzelm@14815
    57
structure Output: 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@23616
    69
  val modes = ref (Symtab.make [("", default)]);
wenzelm@23616
    70
in
wenzelm@23616
    71
  fun add_mode name output escape =
wenzelm@23616
    72
    change modes (Symtab.update_new (name, {output = output, escape = escape}));
wenzelm@23616
    73
  fun get_mode () =
wenzelm@23616
    74
    the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
wenzelm@23616
    75
end;
wenzelm@14815
    76
wenzelm@19265
    77
fun output_width x = #output (get_mode ()) x;
wenzelm@14815
    78
val output = #1 o output_width;
wenzelm@23727
    79
wenzelm@23616
    80
fun escape x = #escape (get_mode ()) x;
wenzelm@23727
    81
val escape_malformed = escape o translate_string output;
wenzelm@14815
    82
wenzelm@14815
    83
wenzelm@14815
    84
wenzelm@14815
    85
(** output channels **)
wenzelm@14815
    86
wenzelm@14984
    87
(* output primitives -- normally NOT used directly!*)
wenzelm@14984
    88
wenzelm@14815
    89
fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
wenzelm@14815
    90
fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
wenzelm@14815
    91
wenzelm@14984
    92
val immediate_output = std_output o output;
wenzelm@14815
    93
val writeln_default = std_output o suffix "\n";
wenzelm@14815
    94
wenzelm@14984
    95
wenzelm@14984
    96
(* Isabelle output channels *)
wenzelm@14984
    97
wenzelm@14815
    98
val writeln_fn = ref writeln_default;
wenzelm@14815
    99
val priority_fn = ref (fn s => ! writeln_fn s);
wenzelm@14815
   100
val tracing_fn = ref (fn s => ! writeln_fn s);
wenzelm@14815
   101
val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
wenzelm@14815
   102
val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
aspinall@15190
   103
val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
wenzelm@14815
   104
wenzelm@14815
   105
fun writeln s = ! writeln_fn (output s);
wenzelm@14815
   106
fun priority s = ! priority_fn (output s);
wenzelm@14815
   107
fun tracing s = ! tracing_fn (output s);
wenzelm@14815
   108
fun warning s = ! warning_fn (output s);
aspinall@15190
   109
wenzelm@22826
   110
val tolerate_legacy_features = ref true;
wenzelm@22826
   111
fun legacy_feature s =
wenzelm@22826
   112
  (if ! tolerate_legacy_features then warning else error) ("Legacy feature: " ^ s);
wenzelm@22826
   113
wenzelm@16191
   114
fun no_warnings f = setmp warning_fn (K ()) f;
wenzelm@16191
   115
wenzelm@22130
   116
val debugging = ref false;
wenzelm@22130
   117
fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
aspinall@15190
   118
wenzelm@14815
   119
fun error_msg s = ! error_fn (output s);
wenzelm@18682
   120
wenzelm@20926
   121
val ml_output = (writeln, error_msg);
wenzelm@20926
   122
wenzelm@14815
   123
wenzelm@18682
   124
(* toplevel errors *)
wenzelm@14815
   125
wenzelm@18682
   126
exception TOPLEVEL_ERROR;
wenzelm@18682
   127
wenzelm@18682
   128
val do_toplevel_errors = ref true;
wenzelm@14815
   129
wenzelm@18682
   130
fun toplevel_errors f x =
wenzelm@18682
   131
  if ! do_toplevel_errors then
wenzelm@18682
   132
    f x handle ERROR msg => (error_msg msg; raise TOPLEVEL_ERROR)
wenzelm@18682
   133
  else f x;
wenzelm@14815
   134
wenzelm@18716
   135
fun ML_errors f = setmp do_toplevel_errors true (toplevel_errors f);
wenzelm@18716
   136
wenzelm@18682
   137
wenzelm@14815
   138
wenzelm@14815
   139
(** timing **)
wenzelm@14815
   140
wenzelm@14869
   141
(*global timing mode*)
wenzelm@14869
   142
val timing = ref false;
wenzelm@14869
   143
wenzelm@23862
   144
(*conditional timing*)
wenzelm@14815
   145
fun cond_timeit flag f =
wenzelm@14815
   146
  if flag then
wenzelm@23862
   147
    let
wenzelm@23862
   148
      val start = start_timing ();
wenzelm@23862
   149
      val result = f ();
wenzelm@22585
   150
    in warning (end_timing start); result end
wenzelm@14815
   151
  else f ();
wenzelm@14815
   152
wenzelm@23862
   153
(*unconditional timing*)
wenzelm@14815
   154
fun timeit x = cond_timeit true x;
wenzelm@14815
   155
wenzelm@14815
   156
(*timed application function*)
wenzelm@14815
   157
fun timeap f x = timeit (fn () => f x);
wenzelm@22585
   158
fun timeap_msg s f x = (warning s; timeap f x);
wenzelm@14815
   159
wenzelm@14978
   160
wenzelm@14978
   161
(* accumulated timing *)
wenzelm@14978
   162
wenzelm@14978
   163
local
wenzelm@14978
   164
wenzelm@14978
   165
datatype time_info = TI of
wenzelm@16726
   166
  {name: string,
wenzelm@16726
   167
   timer: Timer.cpu_timer,
wenzelm@14978
   168
   sys: Time.time,
wenzelm@14978
   169
   usr: Time.time,
wenzelm@14978
   170
   gc: Time.time,
wenzelm@14978
   171
   count: int};
wenzelm@14978
   172
wenzelm@16726
   173
fun time_init name = ref (TI
wenzelm@16726
   174
 {name = name,
wenzelm@16726
   175
  timer = Timer.startCPUTimer (),
wenzelm@16726
   176
  sys = Time.zeroTime,
wenzelm@16726
   177
  usr = Time.zeroTime,
wenzelm@16726
   178
  gc = Time.zeroTime,
wenzelm@16726
   179
  count = 0});
wenzelm@14978
   180
wenzelm@16726
   181
fun time_reset (r as ref (TI {name, ...})) = r := ! (time_init name);
wenzelm@14978
   182
wenzelm@14978
   183
fun time_check (ref (TI r)) = r;
wenzelm@14978
   184
wenzelm@16726
   185
fun time_add ti f x =
wenzelm@14978
   186
  let
wenzelm@16726
   187
    fun add_diff time time1 time2 =
wenzelm@16726
   188
      Time.+ (time, Time.- (time2, time1) handle Time.Time => Time.zeroTime);
wenzelm@16726
   189
    val {name, timer, sys, usr, gc, count} = time_check ti;
wenzelm@21295
   190
    val (sys1, usr1, gc1) = check_timer timer;
wenzelm@14978
   191
    val result = capture f x;
wenzelm@21295
   192
    val (sys2, usr2, gc2) = check_timer timer;
wenzelm@14978
   193
  in
wenzelm@16726
   194
    ti := TI
wenzelm@16726
   195
     {name = name,
wenzelm@16726
   196
      timer = timer,
wenzelm@16726
   197
      sys = add_diff sys sys1 sys2,
wenzelm@16726
   198
      usr = add_diff usr usr1 usr2,
wenzelm@16726
   199
      gc = add_diff gc gc1 gc2,
wenzelm@14978
   200
      count = count + 1};
wenzelm@14978
   201
    release result
wenzelm@14978
   202
  end;
wenzelm@14978
   203
wenzelm@16726
   204
fun time_finish ti =
wenzelm@16726
   205
  let
wenzelm@16726
   206
    fun secs prfx time = prfx ^ Time.toString time;
wenzelm@16726
   207
    val {name, timer, sys, usr, gc, count} = time_check ti;
wenzelm@16726
   208
  in
wenzelm@22585
   209
    warning ("Total of " ^ quote name ^ ": " ^
wenzelm@16726
   210
      secs "User " usr ^ secs "  GC " gc ^ secs "  All " (Time.+ (sys, Time.+ (usr, gc))) ^
wenzelm@16726
   211
      " secs in " ^ string_of_int count ^ " calls");
wenzelm@16726
   212
    time_reset ti
wenzelm@16726
   213
  end;
wenzelm@16726
   214
wenzelm@16726
   215
val time_finish_hooks = ref ([]: (unit -> unit) list);
wenzelm@16726
   216
wenzelm@16726
   217
in
wenzelm@16726
   218
wenzelm@16726
   219
fun time_accumulator name =
wenzelm@16726
   220
  let val ti = time_init name in
wenzelm@16726
   221
    change time_finish_hooks (cons (fn () => time_finish ti));
wenzelm@16726
   222
    time_add ti
wenzelm@16726
   223
  end;
wenzelm@16726
   224
wenzelm@16726
   225
fun accumulated_time () = List.app (fn f => f ()) (! time_finish_hooks);
wenzelm@16726
   226
wenzelm@14978
   227
end;
wenzelm@14978
   228
wenzelm@14815
   229
end;
wenzelm@14815
   230
wenzelm@14815
   231
structure BasicOutput: BASIC_OUTPUT = Output;
wenzelm@14815
   232
open BasicOutput;