# HG changeset patch
# User berghofe
# Date 1097484679 -7200
# Node ID 250e9be7a09d2101c1cea631cdb1e177b25511b7
# Parent  f289e8ba2bb343d0f88de910dedb485edf5f8fba
Some changes to allow skipping of proof scripts.

diff -r f289e8ba2bb3 -r 250e9be7a09d src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Oct 11 07:42:22 2004 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Oct 11 10:51:19 2004 +0200
@@ -129,15 +129,18 @@
 
 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
 val clear_undos_theory = Toplevel.history o History.clear;
-val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo;
+val redo = Toplevel.history History.redo o Toplevel.proof'' ProofHistory.redo o
+  Toplevel.skip_proof History.redo;
 
-fun undos_proof n = Toplevel.proof (fn prf =>
-  if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf);
+fun undos_proof n = Toplevel.proof'' (fn prf =>
+    if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf) o
+  Toplevel.skip_proof (fn h =>
+    if History.is_initial h then raise Toplevel.UNDEF else funpow n History.undo h);
 
 fun kill_proof_notify (f: unit -> unit) = Toplevel.history (fn hist =>
   (case History.current hist of
     Toplevel.Theory _ => raise Toplevel.UNDEF
-  | Toplevel.Proof _ => (f (); History.undo hist)));
+  | _ => (f (); History.undo hist)));
 
 val kill_proof = kill_proof_notify (K ());
 
diff -r f289e8ba2bb3 -r 250e9be7a09d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Oct 11 07:42:22 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Oct 11 10:51:19 2004 +0200
@@ -483,7 +483,8 @@
 
 val proofP =
   OuterSyntax.command "proof" "backward proof" K.prf_block
-    (Scan.option P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
+    (Scan.option P.method >> (fn m => Toplevel.print o Toplevel.proof (IsarThy.proof m) o
+      Toplevel.skip_proof (History.apply (fn i => i + 1))));
 
 
 (* calculational proof commands *)
diff -r f289e8ba2bb3 -r 250e9be7a09d src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Mon Oct 11 07:42:22 2004 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Mon Oct 11 10:51:19 2004 +0200
@@ -446,6 +446,8 @@
 (* local endings *)
 
 val local_qed = proof'' o (ProofHistory.applys oo Method.local_qed true);
+val skip_local_qed =
+  Toplevel.skip_proof (History.apply (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF));
 val local_terminal_proof = proof'' o (ProofHistory.applys oo Method.local_terminal_proof);
 val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
 val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
@@ -469,6 +471,7 @@
   end);
 
 fun global_qed m = global_result (K (Method.global_qed true m));
+val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1 o History.current);
 fun global_terminal_proof m = global_result (K (Method.global_terminal_proof m));
 val global_default_proof = global_result (K Method.global_default_proof);
 val global_immediate_proof = global_result (K Method.global_immediate_proof);
@@ -478,13 +481,14 @@
 
 (* common endings *)
 
-fun qed meth = local_qed meth o global_qed meth;
+fun qed meth = local_qed meth o global_qed meth o skip_local_qed o skip_global_qed;
 fun terminal_proof meths = local_terminal_proof meths o global_terminal_proof meths;
 val default_proof = local_default_proof o global_default_proof;
 val immediate_proof = local_immediate_proof o global_immediate_proof;
 val done_proof = local_done_proof o global_done_proof;
 val skip_proof = local_skip_proof o global_skip_proof;
-val forget_proof = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current);
+val forget_proof = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current) o
+  Toplevel.skip_proof_to_theory (K true);
 
 
 (* calculational proof commands *)
diff -r f289e8ba2bb3 -r 250e9be7a09d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Oct 11 07:42:22 2004 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Oct 11 10:51:19 2004 +0200
@@ -8,6 +8,7 @@
 signature TOPLEVEL =
 sig
   datatype node = Theory of theory | Proof of ProofHistory.T
+    | SkipProof of int History.T * theory
   type state
   val toplevel: state
   val is_toplevel: state -> bool
@@ -50,13 +51,17 @@
   val imperative: (unit -> unit) -> transition -> transition
   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
     -> transition -> transition
+  val skip_proofs: bool ref
   val theory: (theory -> theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
   val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
   val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
   val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
+  val proof'': (ProofHistory.T -> ProofHistory.T) -> transition -> transition
   val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
   val proof_to_theory': (bool -> ProofHistory.T -> theory) -> transition -> transition
+  val skip_proof: (int History.T -> int History.T) -> transition -> transition
+  val skip_proof_to_theory: (int History.T -> bool) -> transition -> transition
   val unknown_theory: transition -> transition
   val unknown_proof: transition -> transition
   val unknown_context: transition -> transition
@@ -84,10 +89,11 @@
 
 datatype node =
   Theory of theory |
-  Proof of ProofHistory.T;
+  Proof of ProofHistory.T |
+  SkipProof of int History.T * theory;
 
 fun str_of_node (Theory _) = "in theory mode"
-  | str_of_node (Proof _) = "in proof mode";
+  | str_of_node _ = "in proof mode";
 
 fun pretty_context thy = [Pretty.block
   [Pretty.str "theory", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
@@ -96,10 +102,12 @@
 fun pretty_prf prf = Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf);
 
 fun pretty_node_context (Theory thy) = pretty_context thy
-  | pretty_node_context (Proof prf) = pretty_context (Proof.theory_of (ProofHistory.current prf));
+  | pretty_node_context (Proof prf) = pretty_context (Proof.theory_of (ProofHistory.current prf))
+  | pretty_node_context _ = [];
 
 fun pretty_node prf_only (Theory thy) = if prf_only then [] else pretty_context thy
-  | pretty_node _ (Proof prf) = pretty_prf prf;
+  | pretty_node _ (Proof prf) = pretty_prf prf
+  | pretty_node _ _ = [];
 
 
 (* datatype state *)
@@ -156,6 +164,7 @@
 fun node_case f g state =
   (case node_of state of
     Theory thy => f thy
+  | SkipProof (i, thy) => f thy
   | Proof prf => g (ProofHistory.current prf));
 
 val theory_of = node_case I Proof.theory_of;
@@ -357,15 +366,38 @@
     (fn Theory thy => exit thy | _ => raise UNDEF)
     (fn Theory thy => kill thy | _ => raise UNDEF);
 
+(*
+The skip_proofs flag allows proof scripts to be skipped during interactive
+proof in order to speed up processing of large theories. While in skipping
+mode, states are represented as SkipProof (h, thy), where h contains a
+counter for the number of open proof blocks.
+*)
+
+val skip_proofs = ref false;
+
 fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF));
 fun theory' f = app_current (fn int => (fn Theory thy => Theory (f int thy) | _ => raise UNDEF));
-fun theory_to_proof f =
-  app_current (fn int => (fn Theory thy => Proof (f int thy) | _ => raise UNDEF));
-fun proof' f = map_current (fn int => (fn Proof prf => Proof (f int prf) | _ => raise UNDEF));
+fun theory_to_proof f = app_current (fn int =>
+  (fn Theory thy =>
+        if !skip_proofs then SkipProof (History.init (undo_limit int) 0,
+          fst (SkipProof.global_skip_proof int (ProofHistory.current (f int thy))))
+        else Proof (f int thy)
+    | _ => raise UNDEF));
+fun proof''' b f = map_current (fn int => (fn Proof prf => Proof (f int prf)
+  | SkipProof (h, thy) => if b then SkipProof (History.apply I h, thy) else raise UNDEF
+  | _ => raise UNDEF));
+val proof' = proof''' true;
 val proof = proof' o K;
+val proof'' = proof''' false o K;
 fun proof_to_theory' f =
-  map_current (fn int => (fn Proof prf => Theory (f int prf) | _ => raise UNDEF));
+  map_current (fn int => (fn Proof prf => Theory (f int prf)
+    | SkipProof (h, thy) => if History.current h = 0 then Theory thy else raise UNDEF
+    | _ => raise UNDEF));
 val proof_to_theory = proof_to_theory' o K;
+fun skip_proof f = map_current (fn int =>
+  (fn SkipProof (h, thy) => SkipProof (f h, thy) | _ => raise UNDEF));
+fun skip_proof_to_theory p = map_current (fn int =>
+  (fn SkipProof (h, thy) => if p h then Theory thy else raise UNDEF | _ => raise UNDEF));
 
 val unknown_theory = imperative (fn () => warning "Unknown theory context");
 val unknown_proof = imperative (fn () => warning "Unknown proof context");