# HG changeset patch
# User wenzelm
# Date 1006986707 -3600
# Node ID 72348ff7d4a078dc6cc88106b7b408d92af13fe9
# Parent  fed7bed97293f3989b8e8247fe1aaa60e79bc49f
skip_proof: do not require quick_and_dirty in interactive mode;

diff -r fed7bed97293 -r 72348ff7d4a0 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Nov 28 23:30:59 2001 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Wed Nov 28 23:31:47 2001 +0100
@@ -423,8 +423,7 @@
           |> cat_lines |> warning;
         val check =
           (fn () => Seq.pull (SkipProof.local_skip_proof (K (K ()),
-            fn _ => fn thm => rule := Some thm) state))
-          |> Library.setmp quick_and_dirty true
+            fn _ => fn thm => rule := Some thm) true state))
           |> Library.setmp proofs 0
           |> Library.transform_error;
         val result = (check (), None) handle Interrupt => raise Interrupt | e => (None, Some e);
@@ -533,17 +532,18 @@
 
 val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
 val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
-val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof);
 val local_done_proof = proof'' (ProofHistory.applys o Method.local_done_proof);
+val local_skip_proof = Toplevel.proof' (fn int =>
+  ProofHistory.applys (SkipProof.local_skip_proof (cond_print_result_rule int) int));
 
 
 (* global endings *)
 
-fun global_result finish = Toplevel.proof_to_theory (fn prf =>
+fun global_result finish = Toplevel.proof_to_theory' (fn int => fn prf =>
   let
     val state = ProofHistory.current prf;
     val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
-    val (thy, ((kind, name), res)) = finish state;
+    val (thy, ((kind, name), res)) = finish int state;
   in
     if kind = "" orelse kind = Drule.internalK then ()
     else (print_result (Proof.context_of state) ((kind, name), res);
@@ -551,12 +551,13 @@
     thy
   end);
 
-val global_qed = global_result o Method.global_qed true o apsome Comment.ignore_interest;
-val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests;
-val global_default_proof = global_result Method.global_default_proof;
-val global_immediate_proof = global_result Method.global_immediate_proof;
+fun global_qed m = global_result (K (Method.global_qed true (apsome Comment.ignore_interest m)));
+fun global_terminal_proof m =
+  global_result (K (Method.global_terminal_proof (ignore_interests m)));
+val global_default_proof = global_result (K Method.global_default_proof);
+val global_immediate_proof = global_result (K Method.global_immediate_proof);
 val global_skip_proof = global_result SkipProof.global_skip_proof;
-val global_done_proof = global_result Method.global_done_proof;
+val global_done_proof = global_result (K Method.global_done_proof);
 
 
 (* common endings *)
diff -r fed7bed97293 -r 72348ff7d4a0 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Wed Nov 28 23:30:59 2001 +0100
+++ b/src/Pure/Isar/skip_proof.ML	Wed Nov 28 23:31:47 2001 +0100
@@ -13,8 +13,9 @@
   val cheat_tac: theory -> tactic
   val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
   val local_skip_proof: (Proof.context -> string * (string * thm list) list -> unit) *
-    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
-  val global_skip_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
+    (Proof.context -> thm -> unit) -> bool -> Proof.state -> Proof.state Seq.seq
+  val global_skip_proof:
+    bool -> Proof.state -> theory * ((string * string) * (string * thm list) list)
   val setup: (theory -> theory) list
 end;
 
@@ -36,7 +37,7 @@
 
 fun skip_proof (_, SkipProof t) =
   if ! quick_and_dirty then t
-  else error "Proofs may be skipped in quick_and_dirty mode only!";
+  else error "Proof may be skipped in quick_and_dirty mode only!";
 
 val setup = [Theory.add_oracle (skip_proofN, skip_proof)];
 
@@ -57,10 +58,11 @@
 
 (* "sorry" proof command *)
 
-fun cheating ctxt = Method.METHOD (K (cheat_tac (ProofContext.theory_of ctxt)));
+fun cheating int ctxt = Method.METHOD (K (setmp quick_and_dirty (int orelse ! quick_and_dirty)
+    (cheat_tac (ProofContext.theory_of ctxt))));
 
-val local_skip_proof = Method.local_terminal_proof (Method.Basic cheating, None);
-val global_skip_proof = Method.global_terminal_proof (Method.Basic cheating, None);
+fun local_skip_proof x int = Method.local_terminal_proof (Method.Basic (cheating int), None) x;
+fun global_skip_proof int = Method.global_terminal_proof (Method.Basic (cheating int), None);
 
 end;