src/Pure/Isar/toplevel.ML

   val prompt_state_fn: (state -> string) ref
   val print_state_context: state -> unit
   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
   val interact: bool ref
   val timing: bool ref

 and fail_msg detailed kind ((name, pos), exn) =
   "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn;
 
 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;
 
 
 (* controlled execution *)

 fun >> tr =
   (case apply true tr (get_state ()) of
     NONE => false
   | SOME (state', exn_info) =>
       (global_state := (state', exn_info);
-        print_exn exn_info;
+        !print_exn_fn exn_info;
         true));
 
 fun >>> [] = ()
   | >>> (tr :: trs) = if >> tr then >>> trs else ();