--- 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 *)