# HG changeset patch # User wenzelm # Date 1085835250 -7200 # Node ID 77a509d83163cee3c084bd7d969b545ac78447ec # Parent c6b91c8aee1db54423cbdd7eb7e1353caaa3bec4 output channels; diff -r c6b91c8aee1d -r 77a509d83163 src/Pure/General/output.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/output.ML Sat May 29 14:54:10 2004 +0200 @@ -0,0 +1,214 @@ +(* Title: Pure/General/output.ML + ID: $Id$ + Author: Makarius, Hagia Maria Sion Abbey (Jerusalem) + License: GPL (GNU GENERAL PUBLIC LICENSE) + +Output channels and diagnostics messages. +*) + +signature BASIC_OUTPUT = +sig + val print_mode: string list ref + val std_output: string -> unit + val std_error: string -> unit + val writeln_default: string -> unit + val writeln_fn: (string -> unit) ref + val priority_fn: (string -> unit) ref + val tracing_fn: (string -> unit) ref + val warning_fn: (string -> unit) ref + val error_fn: (string -> unit) ref + val writeln: string -> unit + val priority: string -> unit + val tracing: string -> unit + val warning: string -> unit + val error_msg: string -> unit + val error: string -> 'a + val sys_error: string -> 'a + val assert: bool -> string -> unit + val deny: bool -> string -> unit + val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit + val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list + datatype 'a error = Error of string | OK of 'a + val get_error: 'a error -> string option + val get_ok: 'a error -> 'a option + datatype 'a result = Result of 'a | Exn of exn + val get_result: 'a result -> 'a option + val get_exn: 'a result -> exn option + val handle_error: ('a -> 'b) -> 'a -> 'b error + exception ERROR_MESSAGE of string + val transform_error: ('a -> 'b) -> 'a -> 'b + val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b + val cond_timeit: bool -> (unit -> 'a) -> 'a + val timeit: (unit -> 'a) -> 'a + val timeap: ('a -> 'b) -> 'a -> 'b + val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b + val timing: bool ref +end; + +signature OUTPUT = +sig + include BASIC_OUTPUT + exception MISSING_DEFAULT_OUTPUT + val output_width: string -> string * real + val output: string -> string + val indent: string * int -> string + val raw: string -> string + val add_mode: string -> + (string -> string * real) * (string * int -> string) * (string -> string) -> unit +end; + +structure Output: OUTPUT = +struct + +(** print modes **) + +val print_mode = ref ([]: string list); + +val modes = ref (Symtab.empty: + ((string -> string * real) * (string * int -> string) * (string -> string)) + Symtab.table); + +exception MISSING_DEFAULT_OUTPUT; + +fun lookup_mode name = Symtab.lookup (! modes, name); + +fun get_mode () = + (case Library.get_first lookup_mode (! print_mode) of Some p => p + | None => + (case lookup_mode "" of Some p => p + | None => raise MISSING_DEFAULT_OUTPUT)); + +fun output_width x = #1 (get_mode ()) x; +val output = #1 o output_width; +fun indent x = #2 (get_mode ()) x; +fun raw x = #3 (get_mode ()) x; + + + +(** output channels **) + +(*process channels -- normally NOT used directly!*) +fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); +fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr); + +val writeln_default = std_output o suffix "\n"; + +(*hooks for Isabelle channels*) +val writeln_fn = ref writeln_default; +val priority_fn = ref (fn s => ! writeln_fn s); +val tracing_fn = ref (fn s => ! writeln_fn s); +val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### "); +val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** "); + +fun writeln s = ! writeln_fn (output s); +fun priority s = ! priority_fn (output s); +fun tracing s = ! tracing_fn (output s); +fun warning s = ! warning_fn (output s); +fun error_msg s = ! error_fn (output s); + + +(* add_mode *) + +fun add_mode name m = + (if is_none (lookup_mode name) then () + else warning ("Redeclaration of symbol print mode: " ^ quote name); + modes := Symtab.update ((name, m), ! modes)); + + +(* error/warning forms *) + +fun error s = (error_msg s; raise ERROR); +fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg); + +fun assert p msg = if p then () else error msg; +fun deny p msg = if p then error msg else (); + +(*Assert pred for every member of l, generating a message if pred fails*) +fun assert_all pred l msg_fn = + let fun asl [] = () + | asl (x::xs) = if pred x then asl xs else error (msg_fn x) + in asl l end; + +fun overwrite_warn (args as (alist, (a, _))) msg = + (if is_none (assoc (alist, a)) then () else warning msg; + overwrite args); + + + +(** handle errors **) + +datatype 'a error = + Error of string | + OK of 'a; + +fun get_error (Error msg) = Some msg + | get_error _ = None; + +fun get_ok (OK x) = Some x + | get_ok _ = None; + +datatype 'a result = + Result of 'a | + Exn of exn; + +fun get_result (Result x) = Some x + | get_result _ = None; + +fun get_exn (Exn exn) = Some exn + | get_exn _ = None; + +fun handle_error f x = + let + val buffer = ref ([]: string list); + fun capture s = buffer := ! buffer @ [s]; + fun err_msg () = if not (null (! buffer)) then error_msg (cat_lines (! buffer)) else (); + in + (case Result (setmp error_fn capture f x) handle exn => Exn exn of + Result y => (err_msg (); OK y) + | Exn ERROR => Error (cat_lines (! buffer)) + | Exn exn => (err_msg (); raise exn)) + end; + + +(* transform ERROR into ERROR_MESSAGE *) + +exception ERROR_MESSAGE of string; + +fun transform_error f x = + (case handle_error f x of + OK y => y + | Error msg => raise ERROR_MESSAGE msg); + + +(* transform any exception, including ERROR *) + +fun transform_failure exn f x = + transform_error f x handle Interrupt => raise Interrupt | e => raise exn e; + + + +(** timing **) + +(*a conditional timing function: applies f to () and, if the flag is true, + prints its runtime on warning channel*) +fun cond_timeit flag f = + if flag then + let val start = startTiming() + val result = f () + in warning (endTiming start); result end + else f (); + +(*unconditional timing function*) +fun timeit x = cond_timeit true x; + +(*timed application function*) +fun timeap f x = timeit (fn () => f x); +fun timeap_msg s f x = (warning s; timeap f x); + +(*global timing mode*) +val timing = ref false; + +end; + +structure BasicOutput: BASIC_OUTPUT = Output; +open BasicOutput;