--- /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;