Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
init_theory: Runtime.controlled_execution for proper exception trace etc.;
authorwenzelm
Tue, 17 Nov 2009 15:53:35 +0100
changeset 33727 e2d5d7f51aa3
parent 33726 0878aecbf119
child 33738 b424b3259966
init_theory: Runtime.controlled_execution for proper exception trace etc.;
src/Pure/Isar/toplevel.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/toplevel.ML	Tue Nov 17 14:51:57 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Nov 17 15:53:35 2009 +0100
@@ -302,7 +302,8 @@
 local
 
 fun apply_tr int (Init (_, f, exit)) (State (NONE, _)) =
-      State (SOME (Theory (Context.Theory (Theory.checkpoint (f int)), NONE), exit), NONE)
+      State (SOME (Theory (Context.Theory
+          (Theory.checkpoint (Runtime.controlled_execution f int)), NONE), exit), NONE)
   | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
       State (NONE, prev)
   | apply_tr _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
isabelle