--- a/src/Pure/General/output.ML Thu Jan 19 21:22:20 2006 +0100
+++ b/src/Pure/General/output.ML Thu Jan 19 21:22:21 2006 +0100
@@ -47,6 +47,7 @@
exception TOPLEVEL_ERROR
val do_toplevel_errors: bool ref
val toplevel_errors: ('a -> 'b) -> 'a -> 'b
+ val ML_errors: ('a -> 'b) -> 'a -> 'b
val panic: string -> unit
val info: string -> unit
val debug: string -> unit
@@ -139,6 +140,8 @@
f x handle ERROR msg => (error_msg msg; raise TOPLEVEL_ERROR)
else f x;
+fun ML_errors f = setmp do_toplevel_errors true (toplevel_errors f);
+
(* AList operations *)