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