tuned;
authorwenzelm
Sun Mar 10 00:23:52 2019 +0100 (3 months ago ago)
changeset 700696db51f45b5f9
parent 70068 b9985133805d
child 70070 be04e9a053a7
tuned;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun Mar 10 00:21:34 2019 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Mar 10 00:23:52 2019 +0100
     1.3 @@ -252,11 +252,23 @@
     1.4  
     1.5  (** toplevel transitions **)
     1.6  
     1.7 -(* node transactions -- maintaining stable checkpoints *)
     1.8 +(* primitive transitions *)
     1.9 +
    1.10 +datatype trans =
    1.11 +  (*init theory*)
    1.12 +  Init of unit -> theory |
    1.13 +  (*formal exit of theory*)
    1.14 +  Exit |
    1.15 +  (*peek at state*)
    1.16 +  Keep of bool -> state -> unit |
    1.17 +  (*node transaction and presentation*)
    1.18 +  Transaction of (bool -> node -> node_presentation) * (state -> unit);
    1.19 +
    1.20 +local
    1.21  
    1.22  exception FAILURE of state * exn;
    1.23  
    1.24 -fun apply_transaction f g node =
    1.25 +fun apply f g node =
    1.26    let
    1.27      val node_pr = node_presentation node;
    1.28      val context = cases_proper_node I (Context.Proof o Proof.context_of) node;
    1.29 @@ -273,21 +285,6 @@
    1.30      | SOME exn => raise FAILURE (result, exn))
    1.31    end;
    1.32  
    1.33 -
    1.34 -(* primitive transitions *)
    1.35 -
    1.36 -datatype trans =
    1.37 -  (*init theory*)
    1.38 -  Init of unit -> theory |
    1.39 -  (*formal exit of theory*)
    1.40 -  Exit |
    1.41 -  (*peek at state*)
    1.42 -  Keep of bool -> state -> unit |
    1.43 -  (*node transaction and presentation*)
    1.44 -  Transaction of (bool -> node -> node_presentation) * (state -> unit);
    1.45 -
    1.46 -local
    1.47 -
    1.48  fun apply_tr int trans state =
    1.49    (case (trans, node_of state) of
    1.50      (Init f, Toplevel) =>
    1.51 @@ -296,7 +293,7 @@
    1.52    | (Exit, node as Theory (Context.Theory thy)) =>
    1.53        let
    1.54          val State ((node', pr_ctxt), _) =
    1.55 -          node |> apply_transaction
    1.56 +          node |> apply
    1.57              (fn _ => node_presentation (Theory (Context.Theory (Theory.end_theory thy))))
    1.58              (K ());
    1.59        in State ((Toplevel, pr_ctxt), get_theory node') end
    1.60 @@ -304,7 +301,7 @@
    1.61        Runtime.controlled_execution (try generic_theory_of state)
    1.62          (fn () => (f int state; State (node_presentation node, previous_theory_of state))) ()
    1.63    | (Transaction _, Toplevel) => raise UNDEF
    1.64 -  | (Transaction (f, g), node) => apply_transaction (fn x => f int x) g node
    1.65 +  | (Transaction (f, g), node) => apply (fn x => f int x) g node
    1.66    | _ => raise UNDEF);
    1.67  
    1.68  fun apply_union _ [] state = raise FAILURE (state, UNDEF)