src/Pure/General/output.ML
author haftmann
Tue Sep 20 16:17:34 2005 +0200 (2005-09-20)
changeset 17521 0f1c48de39f5
parent 17412 e26cb20ef0cc
child 17539 b2ce48df4d4c
permissions -rw-r--r--
introduced AList module in favor of assoc etc.
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@14911
     5
Output channels and diagnostic messages.
wenzelm@14815
     6
*)
wenzelm@14815
     7
wenzelm@14815
     8
signature BASIC_OUTPUT =
wenzelm@14815
     9
sig
wenzelm@14815
    10
  val print_mode: string list ref
wenzelm@14815
    11
  val std_output: string -> unit
wenzelm@14815
    12
  val std_error: string -> unit
wenzelm@14984
    13
  val immediate_output: string -> unit
wenzelm@16191
    14
  val writeln_default: string -> unit
wenzelm@16191
    15
  val writeln_fn: (string -> unit) ref
wenzelm@16191
    16
  val priority_fn: (string -> unit) ref
wenzelm@16191
    17
  val tracing_fn: (string -> unit) ref
wenzelm@16191
    18
  val warning_fn: (string -> unit) ref
wenzelm@16191
    19
  val error_fn: (string -> unit) ref
wenzelm@16191
    20
  val panic_fn: (string -> unit) ref
wenzelm@16191
    21
  val info_fn: (string -> unit) ref
wenzelm@16191
    22
  val debug_fn: (string -> unit) ref
wenzelm@16191
    23
  val writeln: string -> unit           (*default output (in messages window)*)
wenzelm@16191
    24
  val priority: string -> unit          (*high-priority (maybe modal/pop-up; must be displayed)*)
wenzelm@16191
    25
  val tracing: string -> unit           (*tracing message (possibly in tracing window)*)
wenzelm@16191
    26
  val warning: string -> unit           (*display warning of non-fatal situation*)
wenzelm@16191
    27
  val error_msg: string -> unit         (*display fatal error (possibly modal msg)*)
wenzelm@16191
    28
  val error: string -> 'a               (*display message as above, raise exn*)
wenzelm@16191
    29
  val sys_error: string -> 'a           (*internal fatal error condition; raise exn*)
wenzelm@16191
    30
  val panic: string -> unit             (*unrecoverable fatal error; exits system!*)
wenzelm@16191
    31
  val info: string -> unit              (*incidental information message (e.g. timing)*)
wenzelm@16191
    32
  val debug: string -> unit             (*internal debug messages*)
wenzelm@16191
    33
  val show_debug_msgs: bool ref
wenzelm@16191
    34
  val no_warnings: ('a -> 'b) -> 'a -> 'b
wenzelm@14815
    35
  val assert: bool -> string -> unit
wenzelm@14815
    36
  val deny: bool -> string -> unit
wenzelm@14815
    37
  val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit
wenzelm@14815
    38
  val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
wenzelm@14815
    39
  datatype 'a error = Error of string | OK of 'a
wenzelm@14815
    40
  val get_error: 'a error -> string option
wenzelm@14815
    41
  val get_ok: 'a error -> 'a option
wenzelm@14815
    42
  val handle_error: ('a -> 'b) -> 'a -> 'b error
wenzelm@14815
    43
  exception ERROR_MESSAGE of string
wenzelm@14815
    44
  val transform_error: ('a -> 'b) -> 'a -> 'b
wenzelm@14815
    45
  val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
wenzelm@14869
    46
  val timing: bool ref
wenzelm@14815
    47
  val cond_timeit: bool -> (unit -> 'a) -> 'a
wenzelm@14815
    48
  val timeit: (unit -> 'a) -> 'a
wenzelm@14815
    49
  val timeap: ('a -> 'b) -> 'a -> 'b
wenzelm@14815
    50
  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
wenzelm@16726
    51
  val time_accumulator: string -> ('a -> 'b) -> 'a -> 'b
wenzelm@14815
    52
end;
wenzelm@14815
    53
wenzelm@14815
    54
signature OUTPUT =
wenzelm@14815
    55
sig
wenzelm@14815
    56
  include BASIC_OUTPUT
wenzelm@14881
    57
  val has_mode: string -> bool
wenzelm@14815
    58
  exception MISSING_DEFAULT_OUTPUT
wenzelm@14815
    59
  val output_width: string -> string * real
wenzelm@14815
    60
  val output: string -> string
wenzelm@14815
    61
  val indent: string * int -> string
wenzelm@14815
    62
  val raw: string -> string
wenzelm@14815
    63
  val add_mode: string ->
wenzelm@14815
    64
    (string -> string * real) * (string * int -> string) * (string -> string) -> unit
wenzelm@16683
    65
  val transform_exceptions: bool ref
wenzelm@16726
    66
  val accumulated_time: unit -> unit
wenzelm@14815
    67
end;
wenzelm@14815
    68
wenzelm@14815
    69
structure Output: OUTPUT =
wenzelm@14815
    70
struct
wenzelm@14815
    71
wenzelm@14815
    72
(** print modes **)
wenzelm@14815
    73
wenzelm@14815
    74
val print_mode = ref ([]: string list);
wenzelm@14815
    75
wenzelm@14881
    76
fun has_mode s = s mem_string ! print_mode;
wenzelm@14881
    77
wenzelm@14955
    78
type mode_fns =
wenzelm@14955
    79
 {output_width: string -> string * real,
wenzelm@14955
    80
  indent: string * int -> string,
wenzelm@14955
    81
  raw: string -> string};
wenzelm@14955
    82
wenzelm@14955
    83
val modes = ref (Symtab.empty: mode_fns Symtab.table);
wenzelm@14815
    84
wenzelm@14815
    85
exception MISSING_DEFAULT_OUTPUT;
wenzelm@14815
    86
wenzelm@17412
    87
fun lookup_mode name = Symtab.lookup (! modes) name;
wenzelm@14815
    88
wenzelm@14815
    89
fun get_mode () =
skalberg@15531
    90
  (case Library.get_first lookup_mode (! print_mode) of SOME p => p
skalberg@15531
    91
  | NONE =>
skalberg@15531
    92
      (case lookup_mode "" of SOME p => p
skalberg@15531
    93
      | NONE => raise MISSING_DEFAULT_OUTPUT));  (*sys_error would require output again!*)
wenzelm@14815
    94
wenzelm@14955
    95
fun output_width x = #output_width (get_mode ()) x;
wenzelm@14815
    96
val output = #1 o output_width;
wenzelm@14955
    97
fun indent x = #indent (get_mode ()) x;
wenzelm@14955
    98
fun raw x = #raw (get_mode ()) x;
wenzelm@14815
    99
wenzelm@14815
   100
wenzelm@14815
   101
wenzelm@14815
   102
(** output channels **)
wenzelm@14815
   103
wenzelm@14984
   104
(* output primitives -- normally NOT used directly!*)
wenzelm@14984
   105
wenzelm@14815
   106
fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
wenzelm@14815
   107
fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
wenzelm@14815
   108
wenzelm@14984
   109
val immediate_output = std_output o output;
wenzelm@14815
   110
val writeln_default = std_output o suffix "\n";
wenzelm@14815
   111
wenzelm@14984
   112
wenzelm@14984
   113
(* Isabelle output channels *)
wenzelm@14984
   114
wenzelm@14815
   115
val writeln_fn = ref writeln_default;
wenzelm@14815
   116
val priority_fn = ref (fn s => ! writeln_fn s);
wenzelm@14815
   117
val tracing_fn = ref (fn s => ! writeln_fn s);
wenzelm@14815
   118
val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
wenzelm@14815
   119
val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
aspinall@14862
   120
val panic_fn = ref (std_output o suffix "\n" o prefix_lines "!!! ");
aspinall@15190
   121
val info_fn = ref (std_output o suffix "\n" o prefix_lines  "+++ ");
aspinall@15190
   122
val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
wenzelm@14815
   123
wenzelm@14815
   124
fun writeln s = ! writeln_fn (output s);
wenzelm@14815
   125
fun priority s = ! priority_fn (output s);
wenzelm@14815
   126
fun tracing s = ! tracing_fn (output s);
wenzelm@14815
   127
fun warning s = ! warning_fn (output s);
aspinall@15190
   128
fun info s = ! info_fn (output s);
aspinall@15190
   129
wenzelm@16191
   130
fun no_warnings f = setmp warning_fn (K ()) f;
wenzelm@16191
   131
aspinall@15190
   132
val show_debug_msgs = ref false;
wenzelm@16191
   133
fun debug s = if ! show_debug_msgs then ! debug_fn (output s) else ()
aspinall@15190
   134
wenzelm@14815
   135
fun error_msg s = ! error_fn (output s);
aspinall@14862
   136
fun panic_msg s = ! panic_fn (output s);
wenzelm@14815
   137
wenzelm@16191
   138
wenzelm@14815
   139
(* add_mode *)
wenzelm@14815
   140
wenzelm@14955
   141
fun add_mode name (f, g, h) =
wenzelm@14815
   142
 (if is_none (lookup_mode name) then ()
wenzelm@14815
   143
  else warning ("Redeclaration of symbol print mode: " ^ quote name);
wenzelm@17412
   144
  modes := Symtab.update (name, {output_width = f, indent = g, raw = h}) (! modes));
wenzelm@14815
   145
wenzelm@14815
   146
wenzelm@14911
   147
(* produce errors *)
wenzelm@14815
   148
wenzelm@14815
   149
fun error s = (error_msg s; raise ERROR);
wenzelm@14815
   150
fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg);
aspinall@14862
   151
fun panic s = (panic_msg ("## SYSTEM EXIT ##\n" ^ s); exit 1);
wenzelm@14815
   152
wenzelm@14815
   153
fun assert p msg = if p then () else error msg;
wenzelm@14815
   154
fun deny p msg = if p then error msg else ();
wenzelm@14815
   155
wenzelm@14815
   156
(*Assert pred for every member of l, generating a message if pred fails*)
wenzelm@14815
   157
fun assert_all pred l msg_fn =
wenzelm@14815
   158
  let fun asl [] = ()
wenzelm@14815
   159
        | asl (x::xs) = if pred x then asl xs else error (msg_fn x)
wenzelm@14815
   160
  in asl l end;
wenzelm@14815
   161
wenzelm@14815
   162
fun overwrite_warn (args as (alist, (a, _))) msg =
haftmann@17521
   163
 (if is_none (AList.lookup (op =) alist a) then () else warning msg;
wenzelm@14815
   164
  overwrite args);
wenzelm@14815
   165
haftmann@17521
   166
fun update_warn eq msg (kv as (key, value)) xs = (
haftmann@17521
   167
  if (not o AList.defined eq xs) key then () else warning msg;
haftmann@17521
   168
  AList.update eq kv xs
haftmann@17521
   169
)
wenzelm@14815
   170
wenzelm@14815
   171
(** handle errors  **)
wenzelm@14815
   172
wenzelm@14815
   173
datatype 'a error =
wenzelm@14815
   174
  Error of string |
wenzelm@14815
   175
  OK of 'a;
wenzelm@14815
   176
skalberg@15531
   177
fun get_error (Error msg) = SOME msg
skalberg@15531
   178
  | get_error _ = NONE;
wenzelm@14815
   179
skalberg@15531
   180
fun get_ok (OK x) = SOME x
skalberg@15531
   181
  | get_ok _ = NONE;
wenzelm@14815
   182
wenzelm@14815
   183
fun handle_error f x =
wenzelm@14815
   184
  let
wenzelm@14815
   185
    val buffer = ref ([]: string list);
wenzelm@14881
   186
    fun store_msg s = buffer := ! buffer @ [raw s];
wenzelm@14815
   187
    fun err_msg () = if not (null (! buffer)) then error_msg (cat_lines (! buffer)) else ();
wenzelm@14815
   188
  in
wenzelm@14869
   189
    (case Result (setmp error_fn store_msg f x) handle exn => Exn exn of
wenzelm@14815
   190
      Result y => (err_msg (); OK y)
wenzelm@14815
   191
    | Exn ERROR => Error (cat_lines (! buffer))
wenzelm@14815
   192
    | Exn exn => (err_msg (); raise exn))
wenzelm@14815
   193
  end;
wenzelm@14815
   194
wenzelm@14815
   195
wenzelm@14815
   196
(* transform ERROR into ERROR_MESSAGE *)
wenzelm@14815
   197
wenzelm@16683
   198
val transform_exceptions = ref true;
wenzelm@16683
   199
wenzelm@14815
   200
exception ERROR_MESSAGE of string;
wenzelm@14815
   201
wenzelm@14815
   202
fun transform_error f x =
wenzelm@16683
   203
  if ! transform_exceptions then
wenzelm@16683
   204
    (case handle_error f x of
wenzelm@16683
   205
      OK y => y
wenzelm@16683
   206
    | Error msg => raise ERROR_MESSAGE msg)
wenzelm@16683
   207
  else f x;
wenzelm@14815
   208
wenzelm@14815
   209
wenzelm@14815
   210
(* transform any exception, including ERROR *)
wenzelm@14815
   211
wenzelm@14815
   212
fun transform_failure exn f x =
wenzelm@16683
   213
  if ! transform_exceptions then
wenzelm@16683
   214
    transform_error f x handle Interrupt => raise Interrupt | e => raise exn e
wenzelm@16683
   215
  else f x;
wenzelm@14815
   216
wenzelm@14815
   217
wenzelm@14815
   218
wenzelm@14815
   219
(** timing **)
wenzelm@14815
   220
wenzelm@14869
   221
(*global timing mode*)
wenzelm@14869
   222
val timing = ref false;
wenzelm@14869
   223
wenzelm@14815
   224
(*a conditional timing function: applies f to () and, if the flag is true,
wenzelm@14815
   225
  prints its runtime on warning channel*)
wenzelm@14815
   226
fun cond_timeit flag f =
wenzelm@14815
   227
  if flag then
wenzelm@14815
   228
    let val start = startTiming()
wenzelm@14815
   229
        val result = f ()
aspinall@15190
   230
    in info (endTiming start); result end
wenzelm@14815
   231
  else f ();
wenzelm@14815
   232
wenzelm@14815
   233
(*unconditional timing function*)
wenzelm@14815
   234
fun timeit x = cond_timeit true x;
wenzelm@14815
   235
wenzelm@14815
   236
(*timed application function*)
wenzelm@14815
   237
fun timeap f x = timeit (fn () => f x);
aspinall@15190
   238
fun timeap_msg s f x = (info s; timeap f x);
wenzelm@14815
   239
wenzelm@14978
   240
wenzelm@14978
   241
(* accumulated timing *)
wenzelm@14978
   242
wenzelm@14978
   243
local
wenzelm@14978
   244
wenzelm@14978
   245
datatype time_info = TI of
wenzelm@16726
   246
  {name: string,
wenzelm@16726
   247
   timer: Timer.cpu_timer,
wenzelm@14978
   248
   sys: Time.time,
wenzelm@14978
   249
   usr: Time.time,
wenzelm@14978
   250
   gc: Time.time,
wenzelm@14978
   251
   count: int};
wenzelm@14978
   252
wenzelm@16726
   253
fun time_init name = ref (TI
wenzelm@16726
   254
 {name = name,
wenzelm@16726
   255
  timer = Timer.startCPUTimer (),
wenzelm@16726
   256
  sys = Time.zeroTime,
wenzelm@16726
   257
  usr = Time.zeroTime,
wenzelm@16726
   258
  gc = Time.zeroTime,
wenzelm@16726
   259
  count = 0});
wenzelm@14978
   260
wenzelm@16726
   261
fun time_reset (r as ref (TI {name, ...})) = r := ! (time_init name);
wenzelm@14978
   262
wenzelm@14978
   263
fun time_check (ref (TI r)) = r;
wenzelm@14978
   264
wenzelm@16726
   265
fun time_add ti f x =
wenzelm@14978
   266
  let
wenzelm@16726
   267
    fun add_diff time time1 time2 =
wenzelm@16726
   268
      Time.+ (time, Time.- (time2, time1) handle Time.Time => Time.zeroTime);
wenzelm@16726
   269
    val {name, timer, sys, usr, gc, count} = time_check ti;
wenzelm@14978
   270
    val (sys1, usr1, gc1) = checkTimer timer;
wenzelm@14978
   271
    val result = capture f x;
wenzelm@14978
   272
    val (sys2, usr2, gc2) = checkTimer timer;
wenzelm@14978
   273
  in
wenzelm@16726
   274
    ti := TI
wenzelm@16726
   275
     {name = name,
wenzelm@16726
   276
      timer = timer,
wenzelm@16726
   277
      sys = add_diff sys sys1 sys2,
wenzelm@16726
   278
      usr = add_diff usr usr1 usr2,
wenzelm@16726
   279
      gc = add_diff gc gc1 gc2,
wenzelm@14978
   280
      count = count + 1};
wenzelm@14978
   281
    release result
wenzelm@14978
   282
  end;
wenzelm@14978
   283
wenzelm@16726
   284
fun time_finish ti =
wenzelm@16726
   285
  let
wenzelm@16726
   286
    fun secs prfx time = prfx ^ Time.toString time;
wenzelm@16726
   287
    val {name, timer, sys, usr, gc, count} = time_check ti;
wenzelm@16726
   288
  in
wenzelm@16726
   289
    info ("Total of " ^ quote name ^ ": " ^
wenzelm@16726
   290
      secs "User " usr ^ secs "  GC " gc ^ secs "  All " (Time.+ (sys, Time.+ (usr, gc))) ^
wenzelm@16726
   291
      " secs in " ^ string_of_int count ^ " calls");
wenzelm@16726
   292
    time_reset ti
wenzelm@16726
   293
  end;
wenzelm@16726
   294
wenzelm@16726
   295
val time_finish_hooks = ref ([]: (unit -> unit) list);
wenzelm@16726
   296
wenzelm@16726
   297
in
wenzelm@16726
   298
wenzelm@16726
   299
fun time_accumulator name =
wenzelm@16726
   300
  let val ti = time_init name in
wenzelm@16726
   301
    change time_finish_hooks (cons (fn () => time_finish ti));
wenzelm@16726
   302
    time_add ti
wenzelm@16726
   303
  end;
wenzelm@16726
   304
wenzelm@16726
   305
fun accumulated_time () = List.app (fn f => f ()) (! time_finish_hooks);
wenzelm@16726
   306
wenzelm@14978
   307
end;
wenzelm@14978
   308
wenzelm@14815
   309
end;
wenzelm@14815
   310
wenzelm@14815
   311
structure BasicOutput: BASIC_OUTPUT = Output;
wenzelm@14815
   312
open BasicOutput;