# HG changeset patch
# User aspinall
# Date 1167854953 -3600
# Node ID fe30893e50f24c79b770f2a2d1137e6cfc74a3ac
# Parent  4bb32c127529cd7ed4da63ec628a2c314ed14876
Expose command failure recovery code for top level.

diff -r 4bb32c127529 -r fe30893e50f2 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Jan 03 21:00:24 2007 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Jan 03 21:09:13 2007 +0100
@@ -33,6 +33,8 @@
   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
@@ -310,10 +312,16 @@
 
 in
 
+
+
 fun exn_message exn = exn_msg (! debug) exn;
 
-fun print_exn NONE = ()
-  | print_exn (SOME (exn, s)) = Output.error_msg (cat_lines [exn_message exn, s]);
+fun print_exn_str NONE = NONE
+  | print_exn_str (SOME (exn, s)) = SOME (cat_lines [exn_message exn, s]);
+
+val print_exn_default = Option.app Output.error_msg o print_exn_str
+
+val print_exn_fn = ref print_exn_default;
 
 end;
 
@@ -739,7 +747,7 @@
     NONE => false
   | SOME (state', exn_info) =>
       (global_state := (state', exn_info);
-        print_exn exn_info;
+        !print_exn_fn exn_info;
         true));
 
 fun >>> [] = ()