src/Pure/Isar/toplevel.ML
changeset 37951 4e2aaf080572
parent 37950 bc285d91041e
child 37953 ddc3b72f9a42
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Jul 24 21:22:21 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Jul 24 21:40:48 2010 +0200
     1.3 @@ -295,7 +295,7 @@
     1.4  datatype trans =
     1.5    Init of string * (bool -> theory) * (theory -> unit) | (*theory name, init, exit*)
     1.6    Exit |                                         (*formal exit of theory -- without committing*)
     1.7 -  CommitExit |                                   (*exit and commit final theory*)
     1.8 +  Commit_Exit |                                  (*exit and commit final theory*)
     1.9    Keep of bool -> state -> unit |                (*peek at state*)
    1.10    Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
    1.11  
    1.12 @@ -306,7 +306,7 @@
    1.13            (Theory.checkpoint (Runtime.controlled_execution f int)), NONE), exit), NONE)
    1.14    | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
    1.15        State (NONE, prev)
    1.16 -  | apply_tr _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
    1.17 +  | apply_tr _ Commit_Exit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
    1.18        (Runtime.controlled_execution exit thy; toplevel)
    1.19    | apply_tr int (Keep f) state =
    1.20        Runtime.controlled_execution (fn x => tap (f int) x) state
    1.21 @@ -648,7 +648,7 @@
    1.22  fun commit_exit pos =
    1.23    name "end" empty
    1.24    |> position pos
    1.25 -  |> add_trans CommitExit
    1.26 +  |> add_trans Commit_Exit
    1.27    |> imperative (fn () => warning "Expected to find finished theory");
    1.28  
    1.29