# HG changeset patch # User wenzelm # Date 1280000448 -7200 # Node ID 4e2aaf080572cde76823066e4b7ae675c8461367 # Parent bc285d91041ec5b17f6ff4f8c8f39d088a2c8e08 tuned; diff -r bc285d91041e -r 4e2aaf080572 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sat Jul 24 21:22:21 2010 +0200 +++ b/src/Pure/Isar/toplevel.ML Sat Jul 24 21:40:48 2010 +0200 @@ -295,7 +295,7 @@ datatype trans = Init of string * (bool -> theory) * (theory -> unit) | (*theory name, init, exit*) Exit | (*formal exit of theory -- without committing*) - CommitExit | (*exit and commit final theory*) + Commit_Exit | (*exit and commit final theory*) Keep of bool -> state -> unit | (*peek at state*) Transaction of (bool -> node -> node) * (state -> unit); (*node transaction and presentation*) @@ -306,7 +306,7 @@ (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))) = + | apply_tr _ Commit_Exit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) = (Runtime.controlled_execution exit thy; toplevel) | apply_tr int (Keep f) state = Runtime.controlled_execution (fn x => tap (f int) x) state @@ -648,7 +648,7 @@ fun commit_exit pos = name "end" empty |> position pos - |> add_trans CommitExit + |> add_trans Commit_Exit |> imperative (fn () => warning "Expected to find finished theory");