src/Pure/Isar/toplevel.ML
changeset 7612 ba11b5db431a
parent 7602 2c0f407f80ce
child 7732 d62523296573
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun Sep 26 16:39:54 1999 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Sep 26 16:41:16 1999 +0200
     1.3 @@ -38,11 +38,13 @@
     1.4    val exit: transition -> transition
     1.5    val kill: transition -> transition
     1.6    val keep: (state -> unit) -> transition -> transition
     1.7 +  val keep': (bool -> state -> unit) -> transition -> transition
     1.8    val history: (node History.T -> node History.T) -> transition -> transition
     1.9    val imperative: (unit -> unit) -> transition -> transition
    1.10    val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
    1.11      -> transition -> transition
    1.12    val theory: (theory -> theory) -> transition -> transition
    1.13 +  val theory': (bool -> theory -> theory) -> transition -> transition
    1.14    val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
    1.15    val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    1.16    val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
    1.17 @@ -219,7 +221,7 @@
    1.18      (*push node; provide exit/kill operation*)
    1.19    Exit |                                        (*pop node*)
    1.20    Kill |                                        (*abort node*)
    1.21 -  Keep of state -> unit |                       (*peek at state*)
    1.22 +  Keep of bool -> state -> unit |               (*peek at state*)
    1.23    History of node History.T -> node History.T | (*history operation (undo etc.)*)
    1.24    MapCurrent of bool -> node -> node |          (*change node, bypassing history*)
    1.25    AppCurrent of bool -> node -> node;           (*change node, recording history*)
    1.26 @@ -237,7 +239,7 @@
    1.27    | apply_tr _ Kill (State []) = raise UNDEF
    1.28    | apply_tr _ Kill (State ((node, (_, kill)) :: nodes)) =
    1.29        (kill (History.current node); State nodes)
    1.30 -  | apply_tr _ (Keep f) state = (exhibit_interrupt f state; state)
    1.31 +  | apply_tr int (Keep f) state = (exhibit_interrupt (f int) state; state)
    1.32    | apply_tr _ (History _) (State []) = raise UNDEF
    1.33    | apply_tr _ (History f) (State ((node, term) :: nodes)) = State ((f node, term) :: nodes)
    1.34    | apply_tr int (MapCurrent f) state = node_trans int false f state
    1.35 @@ -312,11 +314,12 @@
    1.36  fun init f exit kill = add_trans (Init (f, (exit, kill)));
    1.37  val exit = add_trans Exit;
    1.38  val kill = add_trans Kill;
    1.39 -val keep = add_trans o Keep;
    1.40 +val keep' = add_trans o Keep;
    1.41  val history = add_trans o History;
    1.42  val map_current = add_trans o MapCurrent;
    1.43  val app_current = add_trans o AppCurrent;
    1.44  
    1.45 +fun keep f = add_trans (Keep (fn _ => f));
    1.46  fun imperative f = keep (fn _ => f ());
    1.47  
    1.48  fun init_theory f exit kill =
    1.49 @@ -325,6 +328,7 @@
    1.50      (fn Theory thy => kill thy | _ => raise UNDEF);
    1.51  
    1.52  fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF));
    1.53 +fun theory' f = app_current (fn int => (fn Theory thy => Theory (f int thy) | _ => raise UNDEF));
    1.54  fun theory_to_proof f =
    1.55    app_current (fn int => (fn Theory thy => Proof (f int thy) | _ => raise UNDEF));
    1.56  fun proof' f = map_current (fn int => (fn Proof prf => Proof (f int prf) | _ => raise UNDEF));