src/Pure/Isar/toplevel.ML
changeset 60695 044f8bb3dd30
parent 60403 9be917b2f376
child 60895 501be4aa75b4
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Jul 08 12:09:44 2015 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Jul 08 14:30:00 2015 +0200
     1.3 @@ -69,8 +69,9 @@
     1.4    val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
     1.5    val proof: (Proof.state -> Proof.state) -> transition -> transition
     1.6    val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
     1.7 -  val skip_proof: (int -> int) -> transition -> transition
     1.8 -  val skip_proof_to_theory: (int -> bool) -> transition -> transition
     1.9 +  val skip_proof: (unit -> unit) -> transition -> transition
    1.10 +  val skip_proof_open: transition -> transition
    1.11 +  val skip_proof_close: transition -> transition
    1.12    val exec_id: Document_ID.exec -> transition -> transition
    1.13    val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
    1.14    val add_hook: (transition -> state -> state -> unit) -> unit
    1.15 @@ -510,16 +511,24 @@
    1.16  val proofs = proofs' o K;
    1.17  val proof = proof' o K;
    1.18  
    1.19 +
    1.20 +(* skipped proofs *)
    1.21 +
    1.22  fun actual_proof f = transaction (fn _ =>
    1.23    (fn Proof (prf, x) => Proof (f prf, x)
    1.24      | _ => raise UNDEF));
    1.25  
    1.26  fun skip_proof f = transaction (fn _ =>
    1.27 -  (fn Skipped_Proof (h, x) => Skipped_Proof (f h, x)
    1.28 +  (fn skip as Skipped_Proof _ => (f (); skip)
    1.29      | _ => raise UNDEF));
    1.30  
    1.31 -fun skip_proof_to_theory pred = transaction (fn _ =>
    1.32 -  (fn Skipped_Proof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
    1.33 +val skip_proof_open = transaction (fn _ =>
    1.34 +  (fn Skipped_Proof (d, x) => Skipped_Proof (d + 1, x)
    1.35 +    | _ => raise UNDEF));
    1.36 +
    1.37 +val skip_proof_close = transaction (fn _ =>
    1.38 +  (fn Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE)
    1.39 +    | Skipped_Proof (d, x) => Skipped_Proof (d - 1, x)
    1.40      | _ => raise UNDEF));
    1.41  
    1.42