--- a/src/Pure/Isar/toplevel.ML Fri Jan 05 14:30:07 2007 +0100
+++ b/src/Pure/Isar/toplevel.ML Fri Jan 05 14:30:08 2007 +0100
@@ -33,8 +33,6 @@
val print_state_default: bool -> state -> unit
val print_state_fn: (bool -> state -> unit) ref
val print_state: bool -> state -> unit
- val print_exn_fn: ((exn * string) option -> unit) ref
- val print_exn_str: (exn * string) option -> string option
val pretty_state: bool -> state -> Pretty.T list
val quiet: bool ref
val debug: bool ref
@@ -312,16 +310,10 @@
in
-
-
fun exn_message exn = exn_msg (! debug) exn;
-fun print_exn_str NONE = NONE
- | print_exn_str (SOME (exn, s)) = SOME (cat_lines [exn_message exn, s]);
-
-val print_exn_default = K () o Option.map Output.error_msg o print_exn_str
-
-val print_exn_fn = ref print_exn_default;
+fun print_exn NONE = ()
+ | print_exn (SOME (exn, s)) = Output.error_msg (cat_lines [exn_message exn, s]);
end;
@@ -747,7 +739,7 @@
NONE => false
| SOME (state', exn_info) =>
(global_state := (state', exn_info);
- !print_exn_fn exn_info;
+ print_exn exn_info;
true));
fun >>> [] = ()
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Jan 05 14:30:07 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Jan 05 14:30:08 2007 +0100
@@ -206,10 +206,8 @@
info_fn := (fn s => normalmsg Message Information false s);
debug_fn := (fn s => normalmsg Message Internal false s);
warning_fn := (fn s => errormsg Warning s);
- panic_fn := (fn s => errormsg Panic s);
- error_fn := (fn s => errormsg Nonfatal s);
- Toplevel.print_exn_fn := (K () o Option.map (errormsg Fatal) o Toplevel.print_exn_str);
- ())
+ error_fn := (fn s => errormsg Fatal s);
+ panic_fn := (fn s => errormsg Panic s));
(* immediate messages *)
@@ -924,7 +922,7 @@
local
(* Extra command for embedding prover-control inside document (obscure/debug usage). *)
-val process_pgipP =
+val process_pgipP =
OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
(OuterParse.text >> (Toplevel.no_timing oo
(fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
@@ -946,7 +944,7 @@
| init_pgip true =
(! initialized orelse
(setmp warning_fn (K ()) init_outer_syntax ();
- PgipParser.init ();
+ PgipParser.init ();
setup_xsymbols_output ();
setup_pgml_output ();
setup_messages ();