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