skip_proof: do not require quick_and_dirty in interactive mode;
authorwenzelm
Wed Nov 28 23:31:47 2001 +0100 (2001-11-28 ago)
changeset 1231872348ff7d4a0
parent 12317 fed7bed97293
child 12319 cb3ea5750c3b
skip_proof: do not require quick_and_dirty in interactive mode;
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/skip_proof.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Nov 28 23:30:59 2001 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Nov 28 23:31:47 2001 +0100
     1.3 @@ -423,8 +423,7 @@
     1.4            |> cat_lines |> warning;
     1.5          val check =
     1.6            (fn () => Seq.pull (SkipProof.local_skip_proof (K (K ()),
     1.7 -            fn _ => fn thm => rule := Some thm) state))
     1.8 -          |> Library.setmp quick_and_dirty true
     1.9 +            fn _ => fn thm => rule := Some thm) true state))
    1.10            |> Library.setmp proofs 0
    1.11            |> Library.transform_error;
    1.12          val result = (check (), None) handle Interrupt => raise Interrupt | e => (None, Some e);
    1.13 @@ -533,17 +532,18 @@
    1.14  
    1.15  val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
    1.16  val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
    1.17 -val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof);
    1.18  val local_done_proof = proof'' (ProofHistory.applys o Method.local_done_proof);
    1.19 +val local_skip_proof = Toplevel.proof' (fn int =>
    1.20 +  ProofHistory.applys (SkipProof.local_skip_proof (cond_print_result_rule int) int));
    1.21  
    1.22  
    1.23  (* global endings *)
    1.24  
    1.25 -fun global_result finish = Toplevel.proof_to_theory (fn prf =>
    1.26 +fun global_result finish = Toplevel.proof_to_theory' (fn int => fn prf =>
    1.27    let
    1.28      val state = ProofHistory.current prf;
    1.29      val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
    1.30 -    val (thy, ((kind, name), res)) = finish state;
    1.31 +    val (thy, ((kind, name), res)) = finish int state;
    1.32    in
    1.33      if kind = "" orelse kind = Drule.internalK then ()
    1.34      else (print_result (Proof.context_of state) ((kind, name), res);
    1.35 @@ -551,12 +551,13 @@
    1.36      thy
    1.37    end);
    1.38  
    1.39 -val global_qed = global_result o Method.global_qed true o apsome Comment.ignore_interest;
    1.40 -val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests;
    1.41 -val global_default_proof = global_result Method.global_default_proof;
    1.42 -val global_immediate_proof = global_result Method.global_immediate_proof;
    1.43 +fun global_qed m = global_result (K (Method.global_qed true (apsome Comment.ignore_interest m)));
    1.44 +fun global_terminal_proof m =
    1.45 +  global_result (K (Method.global_terminal_proof (ignore_interests m)));
    1.46 +val global_default_proof = global_result (K Method.global_default_proof);
    1.47 +val global_immediate_proof = global_result (K Method.global_immediate_proof);
    1.48  val global_skip_proof = global_result SkipProof.global_skip_proof;
    1.49 -val global_done_proof = global_result Method.global_done_proof;
    1.50 +val global_done_proof = global_result (K Method.global_done_proof);
    1.51  
    1.52  
    1.53  (* common endings *)
     2.1 --- a/src/Pure/Isar/skip_proof.ML	Wed Nov 28 23:30:59 2001 +0100
     2.2 +++ b/src/Pure/Isar/skip_proof.ML	Wed Nov 28 23:31:47 2001 +0100
     2.3 @@ -13,8 +13,9 @@
     2.4    val cheat_tac: theory -> tactic
     2.5    val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
     2.6    val local_skip_proof: (Proof.context -> string * (string * thm list) list -> unit) *
     2.7 -    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
     2.8 -  val global_skip_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
     2.9 +    (Proof.context -> thm -> unit) -> bool -> Proof.state -> Proof.state Seq.seq
    2.10 +  val global_skip_proof:
    2.11 +    bool -> Proof.state -> theory * ((string * string) * (string * thm list) list)
    2.12    val setup: (theory -> theory) list
    2.13  end;
    2.14  
    2.15 @@ -36,7 +37,7 @@
    2.16  
    2.17  fun skip_proof (_, SkipProof t) =
    2.18    if ! quick_and_dirty then t
    2.19 -  else error "Proofs may be skipped in quick_and_dirty mode only!";
    2.20 +  else error "Proof may be skipped in quick_and_dirty mode only!";
    2.21  
    2.22  val setup = [Theory.add_oracle (skip_proofN, skip_proof)];
    2.23  
    2.24 @@ -57,10 +58,11 @@
    2.25  
    2.26  (* "sorry" proof command *)
    2.27  
    2.28 -fun cheating ctxt = Method.METHOD (K (cheat_tac (ProofContext.theory_of ctxt)));
    2.29 +fun cheating int ctxt = Method.METHOD (K (setmp quick_and_dirty (int orelse ! quick_and_dirty)
    2.30 +    (cheat_tac (ProofContext.theory_of ctxt))));
    2.31  
    2.32 -val local_skip_proof = Method.local_terminal_proof (Method.Basic cheating, None);
    2.33 -val global_skip_proof = Method.global_terminal_proof (Method.Basic cheating, None);
    2.34 +fun local_skip_proof x int = Method.local_terminal_proof (Method.Basic (cheating int), None) x;
    2.35 +fun global_skip_proof int = Method.global_terminal_proof (Method.Basic (cheating int), None);
    2.36  
    2.37  end;
    2.38