# HG changeset patch
# User aspinall
# Date 1167855102 -3600
# Node ID 9fb029d1189b0016b1297c732d9d5c2af8e54040
# Parent  fe30893e50f24c79b770f2a2d1137e6cfc74a3ac
Use Isar toplevel print_exn_fn for generating error responses instead of Output.error_msg.

diff -r fe30893e50f2 -r 9fb029d1189b src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jan 03 21:09:13 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jan 03 21:11:42 2007 +0100
@@ -179,6 +179,14 @@
             queue_or_issue pgip
         end
 
+    (* Note: PGIP specifies that any fatal Errorresponse which occurs before <ready/>
+       indicates that the previously sent command has failed. To be 100% accurate we 
+       adjust the Isar top level rather than just using Output.error_msg,
+       otherwise degenerate examples like ML_setup {* Output.error_msg "fake"; *}
+       (and perhaps other examples involving user tactics which print errors) 
+       are wrongly considered to have failed. 
+     *)
+
     fun errormsg fatality s =
         let
               val content = XML.Elem("pgmltext",[],[XML.Rawtext s])
@@ -206,8 +214,11 @@
   info_fn := (fn s => normalmsg Message Information false s);
   debug_fn := (fn s => normalmsg Message Internal false s);
   warning_fn := (fn s => errormsg Nonfatal s);
-  error_fn := (fn s => errormsg Fatal s);
-  panic_fn := (fn s => errormsg Panic s))
+  panic_fn := (fn s => errormsg Panic s);
+  error_fn := (fn s => errormsg Nonfatal s); (* was (fn s => errormsg Fatal s); *)
+  Toplevel.print_exn_fn := (Option.app (errormsg Fatal) o Toplevel.print_exn_str);
+  ())
+
 
 (* immediate messages *)