# HG changeset patch
# User wenzelm
# Date 1137702143 -3600
# Node ID d01837224eaf7fd7c6f71e218a2a8bf9d05a6998
# Parent  6261fcfaca1d18dad66debe3708c46ea1f9c5f63
keep: disable Output.toplevel_errors;
program: Output.ML_errors;

diff -r 6261fcfaca1d -r d01837224eaf src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Jan 19 21:22:22 2006 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Jan 19 21:22:23 2006 +0100
@@ -339,7 +339,8 @@
   | apply_tr _ Kill (State NONE) = raise UNDEF
   | apply_tr _ Kill (State (SOME (node, (_, kill)))) =
       (kill (History.current node); State NONE)
-  | apply_tr int (Keep f) state = (raise_interrupt (f int) state; state)
+  | apply_tr int (Keep f) state =
+      (setmp Output.do_toplevel_errors false (raise_interrupt (f int)) state; state)
   | apply_tr _ (History _) (State NONE) = raise UNDEF
   | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term))
   | apply_tr int (Transaction (hist, f)) state = transaction hist (fn x => f int x) state;
@@ -629,12 +630,10 @@
 end;
 
 
-(* program: independent of state *)
+(* toplevel program: independent of state *)
 
 fun program f =
-  ((fn () => debugging f () handle exn => error (exn_message exn))
-    |> setmp Output.do_toplevel_errors true
-    |> Output.toplevel_errors) ();
+  Output.ML_errors (fn () => debugging f () handle exn => error (exn_message exn)) ();