# HG changeset patch
# User wenzelm
# Date 1168003808 -3600
# Node ID 4b70cbd9600703a96b577cbcff5e09ff8323d873
# Parent  a3519c0c2d8fc029fd05fad6dab3974eb3529d0b
removed Toplevel.print_exn hook -- existing error_msg_fn does the job;

diff -r a3519c0c2d8f -r 4b70cbd96007 src/Pure/Isar/toplevel.ML
--- 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 >>> [] = ()
diff -r a3519c0c2d8f -r 4b70cbd96007 src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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 ();