# HG changeset patch
# User wenzelm
# Date 911472581 -3600
# Node ID 2d7c7a4fcd8ab00f503575b22144124b35220fd2
# Parent  fe7640933a472585ad9cd45342c60eaee70cf5be
break: exhibit state stack;

diff -r fe7640933a47 -r 2d7c7a4fcd8a src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Nov 19 11:49:09 1998 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Nov 19 11:49:41 1998 +0100
@@ -87,6 +87,7 @@
 exception UNDEF;
 
 val toplevel = State [];
+fun append_states (State ns) (State ms) = State (ns @ ms);
 
 fun print_state (State []) = ()
   | print_state (State [(node, _)]) = print_node node
@@ -301,10 +302,11 @@
   Some (transform_interrupt_state (transform_error (app int tr)) state, None)
     handle
       TERMINATE => None
+    | FAIL (exn_info as (BREAK break_state, _)) =>
+        Some (append_states break_state state, Some exn_info)
     | FAIL exn_info => Some (state, Some exn_info)
     | PureThy.ROLLBACK (copy_thy, opt_exn) =>
         Some (rollback tr copy_thy state, apsome (fn exn => (exn, at_command tr)) opt_exn)
-    | exn as BREAK break_state => Some (break_state, Some (exn, at_command tr))
     | exn => Some (state, Some (exn, at_command tr));