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