src/Pure/General/output.ML
changeset 18682 216692feebab
parent 17539 b2ce48df4d4c
child 18716 bb4af2bdd17b
     1.1 --- a/src/Pure/General/output.ML	Sat Jan 14 17:14:14 2006 +0100
     1.2 +++ b/src/Pure/General/output.ML	Sat Jan 14 17:14:15 2006 +0100
     1.3 @@ -12,39 +12,22 @@
     1.4    val std_error: string -> unit
     1.5    val immediate_output: string -> unit
     1.6    val writeln_default: string -> unit
     1.7 -  val writeln_fn: (string -> unit) ref
     1.8 -  val priority_fn: (string -> unit) ref
     1.9 -  val tracing_fn: (string -> unit) ref
    1.10 -  val warning_fn: (string -> unit) ref
    1.11 -  val error_fn: (string -> unit) ref
    1.12 -  val panic_fn: (string -> unit) ref
    1.13 -  val info_fn: (string -> unit) ref
    1.14 -  val debug_fn: (string -> unit) ref
    1.15 -  val writeln: string -> unit           (*default output (in messages window)*)
    1.16 -  val priority: string -> unit          (*high-priority (maybe modal/pop-up; must be displayed)*)
    1.17 -  val tracing: string -> unit           (*tracing message (possibly in tracing window)*)
    1.18 -  val warning: string -> unit           (*display warning of non-fatal situation*)
    1.19 -  val error_msg: string -> unit         (*display fatal error (possibly modal msg)*)
    1.20 -  val error: string -> 'a               (*display message as above, raise exn*)
    1.21 -  val sys_error: string -> 'a           (*internal fatal error condition; raise exn*)
    1.22 -  val panic: string -> unit             (*unrecoverable fatal error; exits system!*)
    1.23 -  val info: string -> unit              (*incidental information message (e.g. timing)*)
    1.24 -  val debug: string -> unit             (*internal debug messages*)
    1.25 +  val writeln_fn: (string -> unit) ref    (*default output (in messages window)*)
    1.26 +  val priority_fn: (string -> unit) ref   (*high-priority (maybe modal/pop-up; must be displayed)*)
    1.27 +  val tracing_fn: (string -> unit) ref    (*tracing message (possibly in tracing window)*)
    1.28 +  val warning_fn: (string -> unit) ref    (*display warning of non-fatal situation*)
    1.29 +  val error_fn: (string -> unit) ref      (*display fatal error (possibly modal msg)*)
    1.30 +  val panic_fn: (string -> unit) ref      (*unrecoverable fatal error; exits system!*)
    1.31 +  val info_fn: (string -> unit) ref       (*incidental information message (e.g. timing)*)
    1.32 +  val debug_fn: (string -> unit) ref      (*internal debug messages*)
    1.33 +  val writeln: string -> unit
    1.34 +  val priority: string -> unit
    1.35 +  val tracing: string -> unit
    1.36 +  val warning: string -> unit
    1.37 +  val update_warn: ('a * 'a -> bool) -> string -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list
    1.38 +  val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
    1.39    val show_debug_msgs: bool ref
    1.40    val no_warnings: ('a -> 'b) -> 'a -> 'b
    1.41 -  val assert: bool -> string -> unit
    1.42 -  val deny: bool -> string -> unit
    1.43 -  val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit
    1.44 -  val update_warn: ('a * 'a -> bool) -> string -> ('a * 'b)
    1.45 -    -> ('a * 'b) list -> ('a * 'b) list
    1.46 -  val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
    1.47 -  datatype 'a error = Error of string | OK of 'a
    1.48 -  val get_error: 'a error -> string option
    1.49 -  val get_ok: 'a error -> 'a option
    1.50 -  val handle_error: ('a -> 'b) -> 'a -> 'b error
    1.51 -  exception ERROR_MESSAGE of string
    1.52 -  val transform_error: ('a -> 'b) -> 'a -> 'b
    1.53 -  val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
    1.54    val timing: bool ref
    1.55    val cond_timeit: bool -> (unit -> 'a) -> 'a
    1.56    val timeit: (unit -> 'a) -> 'a
    1.57 @@ -57,14 +40,19 @@
    1.58  sig
    1.59    include BASIC_OUTPUT
    1.60    val has_mode: string -> bool
    1.61 -  exception MISSING_DEFAULT_OUTPUT
    1.62    val output_width: string -> string * real
    1.63    val output: string -> string
    1.64    val indent: string * int -> string
    1.65    val raw: string -> string
    1.66 +  exception TOPLEVEL_ERROR
    1.67 +  val do_toplevel_errors: bool ref
    1.68 +  val toplevel_errors: ('a -> 'b) -> 'a -> 'b
    1.69 +  val panic: string -> unit
    1.70 +  val info: string -> unit
    1.71 +  val debug: string -> unit
    1.72 +  val error_msg: string -> unit
    1.73    val add_mode: string ->
    1.74      (string -> string * real) * (string * int -> string) * (string -> string) -> unit
    1.75 -  val transform_exceptions: bool ref
    1.76    val accumulated_time: unit -> unit
    1.77  end;
    1.78  
    1.79 @@ -84,9 +72,9 @@
    1.80  
    1.81  val modes = ref (Symtab.empty: mode_fns Symtab.table);
    1.82  
    1.83 -exception MISSING_DEFAULT_OUTPUT;
    1.84 +fun lookup_mode name = Symtab.lookup (! modes) name;
    1.85  
    1.86 -fun lookup_mode name = Symtab.lookup (! modes) name;
    1.87 +exception MISSING_DEFAULT_OUTPUT;
    1.88  
    1.89  fun get_mode () =
    1.90    (case Library.get_first lookup_mode (! print_mode) of SOME p => p
    1.91 @@ -135,31 +123,24 @@
    1.92  fun debug s = if ! show_debug_msgs then ! debug_fn (output s) else ()
    1.93  
    1.94  fun error_msg s = ! error_fn (output s);
    1.95 +
    1.96  fun panic_msg s = ! panic_fn (output s);
    1.97 -
    1.98 -
    1.99 -(* add_mode *)
   1.100 -
   1.101 -fun add_mode name (f, g, h) =
   1.102 - (if is_none (lookup_mode name) then ()
   1.103 -  else warning ("Redeclaration of symbol print mode: " ^ quote name);
   1.104 -  modes := Symtab.update (name, {output_width = f, indent = g, raw = h}) (! modes));
   1.105 +fun panic s = (panic_msg ("## SYSTEM EXIT ##\n" ^ s); exit 1);
   1.106  
   1.107  
   1.108 -(* produce errors *)
   1.109 +(* toplevel errors *)
   1.110  
   1.111 -fun error s = (error_msg s; raise ERROR);
   1.112 -fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg);
   1.113 -fun panic s = (panic_msg ("## SYSTEM EXIT ##\n" ^ s); exit 1);
   1.114 +exception TOPLEVEL_ERROR;
   1.115 +
   1.116 +val do_toplevel_errors = ref true;
   1.117  
   1.118 -fun assert p msg = if p then () else error msg;
   1.119 -fun deny p msg = if p then error msg else ();
   1.120 +fun toplevel_errors f x =
   1.121 +  if ! do_toplevel_errors then
   1.122 +    f x handle ERROR msg => (error_msg msg; raise TOPLEVEL_ERROR)
   1.123 +  else f x;
   1.124  
   1.125 -(*Assert pred for every member of l, generating a message if pred fails*)
   1.126 -fun assert_all pred l msg_fn =
   1.127 -  let fun asl [] = ()
   1.128 -        | asl (x::xs) = if pred x then asl xs else error (msg_fn x)
   1.129 -  in asl l end;
   1.130 +
   1.131 +(* AList operations *)
   1.132  
   1.133  fun overwrite (al, p as (key, _)) =
   1.134    let fun over ((q as (keyi, _)) :: pairs) =
   1.135 @@ -171,56 +152,17 @@
   1.136   (if is_none (AList.lookup (op =) alist a) then () else warning msg;
   1.137    overwrite args);
   1.138  
   1.139 -fun update_warn eq msg (kv as (key, value)) xs = (
   1.140 -  if (not o AList.defined eq xs) key then () else warning msg;
   1.141 -  AList.update eq kv xs
   1.142 -)
   1.143 -
   1.144 -(** handle errors  **)
   1.145 -
   1.146 -datatype 'a error =
   1.147 -  Error of string |
   1.148 -  OK of 'a;
   1.149 -
   1.150 -fun get_error (Error msg) = SOME msg
   1.151 -  | get_error _ = NONE;
   1.152 -
   1.153 -fun get_ok (OK x) = SOME x
   1.154 -  | get_ok _ = NONE;
   1.155 -
   1.156 -fun handle_error f x =
   1.157 -  let
   1.158 -    val buffer = ref ([]: string list);
   1.159 -    fun store_msg s = buffer := ! buffer @ [raw s];
   1.160 -    fun err_msg () = if not (null (! buffer)) then error_msg (cat_lines (! buffer)) else ();
   1.161 -  in
   1.162 -    (case Result (setmp error_fn store_msg f x) handle exn => Exn exn of
   1.163 -      Result y => (err_msg (); OK y)
   1.164 -    | Exn ERROR => Error (cat_lines (! buffer))
   1.165 -    | Exn exn => (err_msg (); raise exn))
   1.166 -  end;
   1.167 +fun update_warn eq msg (kv as (key, value)) xs =
   1.168 + (if (not o AList.defined eq xs) key then () else warning msg;
   1.169 +  AList.update eq kv xs);
   1.170  
   1.171  
   1.172 -(* transform ERROR into ERROR_MESSAGE *)
   1.173 -
   1.174 -val transform_exceptions = ref true;
   1.175 -
   1.176 -exception ERROR_MESSAGE of string;
   1.177 +(* add_mode *)
   1.178  
   1.179 -fun transform_error f x =
   1.180 -  if ! transform_exceptions then
   1.181 -    (case handle_error f x of
   1.182 -      OK y => y
   1.183 -    | Error msg => raise ERROR_MESSAGE msg)
   1.184 -  else f x;
   1.185 -
   1.186 -
   1.187 -(* transform any exception, including ERROR *)
   1.188 -
   1.189 -fun transform_failure exn f x =
   1.190 -  if ! transform_exceptions then
   1.191 -    transform_error f x handle Interrupt => raise Interrupt | e => raise exn e
   1.192 -  else f x;
   1.193 +fun add_mode name (f, g, h) =
   1.194 + (if is_none (lookup_mode name) then ()
   1.195 +  else warning ("Redeclaration of symbol print mode: " ^ quote name);
   1.196 +  modes := Symtab.update (name, {output_width = f, indent = g, raw = h}) (! modes));
   1.197  
   1.198  
   1.199