Merge pull request #559 from hendriktews/omit-proofsHEADmaster

Add feature to omit complete opaque proofs

2 files changed, 33 insertions, 0 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index a517df71..8806774f 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1107,6 +1107,31 @@ It is used:
              (not (string-match "\\`Proof\\s-*\\(\\.\\|\\_<with\\_>\\|\\_<using\\_>\\)" str))))))
 
 
+;; ----- regular expressions for the proof omit feature
+;; see `proof-omit-proofs-configured' in generic/proof-config
+
+(defcustom coq-proof-start-regexp "^Proof\\(\\.\\| \\)"
+  "Value for `proof-script-proof-start-regexp'."
+  :type 'regexp
+  :group 'coq)
+
+(defcustom coq-proof-end-regexp "^\\(Qed\\|Admitted\\)\\."
+  "Value for `proof-script-proof-end-regexp'.
+This is similar to `coq-save-command-regexp-strict' but slightly
+different."
+  :type 'regexp
+  :group 'coq)
+
+(defcustom coq-definition-end-regexp "^\\(Defined\\|Abort\\)\\(\\.\\| \\)"
+  "Value for `proof-script-definition-end-regexp'."
+  :type 'regexp
+  :group 'coq)
+  
+(defcustom coq-omit-proof-admit-command "Admitted."
+  "Value for `proof-script-proof-admit-command'."
+  :type 'string
+  :group 'coq)
+
 ;; ----- keywords for font-lock.
 
 (defvar coq-keywords-kill-goal
diff --git a/coq/coq.el b/coq/coq.el
index 7e8cbd94..1f599345 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1979,6 +1979,14 @@ at `proof-assistant-settings-cmds' evaluation time.")
    proof-tree-find-begin-of-unfinished-proof
      'coq-find-begin-of-unfinished-proof)
 
+  ;; proof-omit-proofs config
+  (setq
+   proof-omit-proofs-configured t
+   proof-script-proof-start-regexp coq-proof-start-regexp
+   proof-script-proof-end-regexp coq-proof-end-regexp
+   proof-script-definition-end-regexp coq-definition-end-regexp
+   proof-script-proof-admit-command coq-omit-proof-admit-command)
+
   (setq proof-cannot-reopen-processed-files nil)
 
   (proof-config-done)