# HG changeset patch
# User wenzelm
# Date 1137702141 -3600
# Node ID bb4af2bdd17bd2aa36ae0836d4163ca6fd7be0ee
# Parent  f809deffdd8fec8a85afb553ae37cf1100e46c3d
added ML_errors;

diff -r f809deffdd8f -r bb4af2bdd17b src/Pure/General/output.ML
--- 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 *)