output channels;
authorwenzelm
Sat May 29 14:54:10 2004 +0200 (2004-05-29)
changeset 1481577a509d83163
parent 14814 c6b91c8aee1d
child 14816 b77cebcd7e6e
output channels;
src/Pure/General/output.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/output.ML	Sat May 29 14:54:10 2004 +0200
     1.3 @@ -0,0 +1,214 @@
     1.4 +(*  Title:      Pure/General/output.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +Output channels and diagnostics messages.
    1.10 +*)
    1.11 +
    1.12 +signature BASIC_OUTPUT =
    1.13 +sig
    1.14 +  val print_mode: string list ref
    1.15 +  val std_output: string -> unit
    1.16 +  val std_error: string -> unit
    1.17 +  val writeln_default: string -> unit
    1.18 +  val writeln_fn: (string -> unit) ref
    1.19 +  val priority_fn: (string -> unit) ref
    1.20 +  val tracing_fn: (string -> unit) ref
    1.21 +  val warning_fn: (string -> unit) ref
    1.22 +  val error_fn: (string -> unit) ref
    1.23 +  val writeln: string -> unit
    1.24 +  val priority: string -> unit
    1.25 +  val tracing: string -> unit
    1.26 +  val warning: string -> unit
    1.27 +  val error_msg: string -> unit
    1.28 +  val error: string -> 'a
    1.29 +  val sys_error: string -> 'a
    1.30 +  val assert: bool -> string -> unit
    1.31 +  val deny: bool -> string -> unit
    1.32 +  val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit
    1.33 +  val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
    1.34 +  datatype 'a error = Error of string | OK of 'a
    1.35 +  val get_error: 'a error -> string option
    1.36 +  val get_ok: 'a error -> 'a option
    1.37 +  datatype 'a result = Result of 'a | Exn of exn
    1.38 +  val get_result: 'a result -> 'a option
    1.39 +  val get_exn: 'a result -> exn option
    1.40 +  val handle_error: ('a -> 'b) -> 'a -> 'b error
    1.41 +  exception ERROR_MESSAGE of string
    1.42 +  val transform_error: ('a -> 'b) -> 'a -> 'b
    1.43 +  val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
    1.44 +  val cond_timeit: bool -> (unit -> 'a) -> 'a
    1.45 +  val timeit: (unit -> 'a) -> 'a
    1.46 +  val timeap: ('a -> 'b) -> 'a -> 'b
    1.47 +  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
    1.48 +  val timing: bool ref
    1.49 +end;
    1.50 +
    1.51 +signature OUTPUT =
    1.52 +sig
    1.53 +  include BASIC_OUTPUT
    1.54 +  exception MISSING_DEFAULT_OUTPUT
    1.55 +  val output_width: string -> string * real
    1.56 +  val output: string -> string
    1.57 +  val indent: string * int -> string
    1.58 +  val raw: string -> string
    1.59 +  val add_mode: string ->
    1.60 +    (string -> string * real) * (string * int -> string) * (string -> string) -> unit
    1.61 +end;
    1.62 +
    1.63 +structure Output: OUTPUT =
    1.64 +struct
    1.65 +
    1.66 +(** print modes **)
    1.67 +
    1.68 +val print_mode = ref ([]: string list);
    1.69 +
    1.70 +val modes = ref (Symtab.empty:
    1.71 +  ((string -> string * real) * (string * int -> string) * (string -> string))
    1.72 +    Symtab.table);
    1.73 +
    1.74 +exception MISSING_DEFAULT_OUTPUT;
    1.75 +
    1.76 +fun lookup_mode name = Symtab.lookup (! modes, name);
    1.77 +
    1.78 +fun get_mode () =
    1.79 +  (case Library.get_first lookup_mode (! print_mode) of Some p => p
    1.80 +  | None =>
    1.81 +      (case lookup_mode "" of Some p => p
    1.82 +      | None => raise MISSING_DEFAULT_OUTPUT));
    1.83 +
    1.84 +fun output_width x = #1 (get_mode ()) x;
    1.85 +val output = #1 o output_width;
    1.86 +fun indent x = #2 (get_mode ()) x;
    1.87 +fun raw x = #3 (get_mode ()) x;
    1.88 +
    1.89 +
    1.90 +
    1.91 +(** output channels **)
    1.92 +
    1.93 +(*process channels -- normally NOT used directly!*)
    1.94 +fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    1.95 +fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
    1.96 +
    1.97 +val writeln_default = std_output o suffix "\n";
    1.98 +
    1.99 +(*hooks for Isabelle channels*)
   1.100 +val writeln_fn = ref writeln_default;
   1.101 +val priority_fn = ref (fn s => ! writeln_fn s);
   1.102 +val tracing_fn = ref (fn s => ! writeln_fn s);
   1.103 +val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
   1.104 +val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
   1.105 +
   1.106 +fun writeln s = ! writeln_fn (output s);
   1.107 +fun priority s = ! priority_fn (output s);
   1.108 +fun tracing s = ! tracing_fn (output s);
   1.109 +fun warning s = ! warning_fn (output s);
   1.110 +fun error_msg s = ! error_fn (output s);
   1.111 +
   1.112 +
   1.113 +(* add_mode *)
   1.114 +
   1.115 +fun add_mode name m =
   1.116 + (if is_none (lookup_mode name) then ()
   1.117 +  else warning ("Redeclaration of symbol print mode: " ^ quote name);
   1.118 +  modes := Symtab.update ((name, m), ! modes));
   1.119 +
   1.120 +
   1.121 +(* error/warning forms *)
   1.122 +
   1.123 +fun error s = (error_msg s; raise ERROR);
   1.124 +fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg);
   1.125 +
   1.126 +fun assert p msg = if p then () else error msg;
   1.127 +fun deny p msg = if p then error msg else ();
   1.128 +
   1.129 +(*Assert pred for every member of l, generating a message if pred fails*)
   1.130 +fun assert_all pred l msg_fn =
   1.131 +  let fun asl [] = ()
   1.132 +        | asl (x::xs) = if pred x then asl xs else error (msg_fn x)
   1.133 +  in asl l end;
   1.134 +
   1.135 +fun overwrite_warn (args as (alist, (a, _))) msg =
   1.136 + (if is_none (assoc (alist, a)) then () else warning msg;
   1.137 +  overwrite args);
   1.138 +
   1.139 +
   1.140 +
   1.141 +(** handle errors  **)
   1.142 +
   1.143 +datatype 'a error =
   1.144 +  Error of string |
   1.145 +  OK of 'a;
   1.146 +
   1.147 +fun get_error (Error msg) = Some msg
   1.148 +  | get_error _ = None;
   1.149 +
   1.150 +fun get_ok (OK x) = Some x
   1.151 +  | get_ok _ = None;
   1.152 +
   1.153 +datatype 'a result =
   1.154 +  Result of 'a |
   1.155 +  Exn of exn;
   1.156 +
   1.157 +fun get_result (Result x) = Some x
   1.158 +  | get_result _ = None;
   1.159 +
   1.160 +fun get_exn (Exn exn) = Some exn
   1.161 +  | get_exn _ = None;
   1.162 +
   1.163 +fun handle_error f x =
   1.164 +  let
   1.165 +    val buffer = ref ([]: string list);
   1.166 +    fun capture s = buffer := ! buffer @ [s];
   1.167 +    fun err_msg () = if not (null (! buffer)) then error_msg (cat_lines (! buffer)) else ();
   1.168 +  in
   1.169 +    (case Result (setmp error_fn capture f x) handle exn => Exn exn of
   1.170 +      Result y => (err_msg (); OK y)
   1.171 +    | Exn ERROR => Error (cat_lines (! buffer))
   1.172 +    | Exn exn => (err_msg (); raise exn))
   1.173 +  end;
   1.174 +
   1.175 +
   1.176 +(* transform ERROR into ERROR_MESSAGE *)
   1.177 +
   1.178 +exception ERROR_MESSAGE of string;
   1.179 +
   1.180 +fun transform_error f x =
   1.181 +  (case handle_error f x of
   1.182 +    OK y => y
   1.183 +  | Error msg => raise ERROR_MESSAGE msg);
   1.184 +
   1.185 +
   1.186 +(* transform any exception, including ERROR *)
   1.187 +
   1.188 +fun transform_failure exn f x =
   1.189 +  transform_error f x handle Interrupt => raise Interrupt | e => raise exn e;
   1.190 +
   1.191 +
   1.192 +
   1.193 +(** timing **)
   1.194 +
   1.195 +(*a conditional timing function: applies f to () and, if the flag is true,
   1.196 +  prints its runtime on warning channel*)
   1.197 +fun cond_timeit flag f =
   1.198 +  if flag then
   1.199 +    let val start = startTiming()
   1.200 +        val result = f ()
   1.201 +    in warning (endTiming start);  result end
   1.202 +  else f ();
   1.203 +
   1.204 +(*unconditional timing function*)
   1.205 +fun timeit x = cond_timeit true x;
   1.206 +
   1.207 +(*timed application function*)
   1.208 +fun timeap f x = timeit (fn () => f x);
   1.209 +fun timeap_msg s f x = (warning s; timeap f x);
   1.210 +
   1.211 +(*global timing mode*)
   1.212 +val timing = ref false;
   1.213 +
   1.214 +end;
   1.215 +
   1.216 +structure BasicOutput: BASIC_OUTPUT = Output;
   1.217 +open BasicOutput;