init_theory: Runtime.controlled_execution for proper exception trace etc.;
authorwenzelm
Tue Nov 17 15:53:35 2009 +0100 (2009-11-17 ago)
changeset 33727e2d5d7f51aa3
parent 33726 0878aecbf119
child 33738 b424b3259966
init_theory: Runtime.controlled_execution for proper exception trace etc.;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Nov 17 14:51:57 2009 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Nov 17 15:53:35 2009 +0100
     1.3 @@ -302,7 +302,8 @@
     1.4  local
     1.5  
     1.6  fun apply_tr int (Init (_, f, exit)) (State (NONE, _)) =
     1.7 -      State (SOME (Theory (Context.Theory (Theory.checkpoint (f int)), NONE), exit), NONE)
     1.8 +      State (SOME (Theory (Context.Theory
     1.9 +          (Theory.checkpoint (Runtime.controlled_execution f int)), NONE), exit), NONE)
    1.10    | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
    1.11        State (NONE, prev)
    1.12    | apply_tr _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =