# 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 >>> [] = ()