diff options
| -rw-r--r-- | CHANGES | 23 | ||||
| -rw-r--r-- | coq/coq-abbrev.el | 16 | ||||
| -rw-r--r-- | coq/coq.el | 64 |
3 files changed, 103 insertions, 0 deletions
@@ -45,6 +45,29 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac compilation does not stop at the first error but rather continues as far as possible. +*** Automatic insertion of "Proof using" annotations. + + When "Suggest Proof Using" is set in coq, coq suggests "Proof + using" annotations when it detects there is no such annotation (or + a wrong one) in you proof and there should be one (i.r. you are + inside a section). By default PG will ask the user before + inserting the suggested annotation. You can customize this + behaviour: + + (setq coq-accept-proof-using-suggestion 'always) + or + (setq coq-accept-proof-using-suggestion 'never) + or (default) + (setq coq-accept-proof-using-suggestion 'ask) + + This is also settable from Coq menu. + + Limitations: + - do not support nested proofs. + - always use the first suggestion (coq can provide several solutions). + - the proof is not replayed, which is consistent with the fact + that pg do not deal with async proofs. + *** Limited extensibility for indentation Coq indentation mechanism is based on a fixed set of tokens and diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 391b1238..0eb707f7 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -113,6 +113,22 @@ :selected (eq proof-three-window-mode-policy 'vertical) :help "One column mode"]) ["Refresh Windows Layout" proof-layout-windows t] + ("Automatic Proof using annotations..." + ["ask" + (customize-set-variable 'coq-accept-proof-using-suggestion 'ask) + :style radio + :selected (eq coq-accept-proof-using-suggestion 'ask) + :help "ask user when a new proof using annotation is suggested"] + ["always" + (customize-set-variable 'coq-accept-proof-using-suggestion 'always) + :style radio + :selected (eq coq-accept-proof-using-suggestion 'always) + :help "Always update the proof using annotation when suggested"] + ["never" + (customize-set-variable 'coq-accept-proof-using-suggestion 'never) + :style radio + :selected (eq coq-accept-proof-using-suggestion 'never) + :help "never update the proof using"]) ["Toggle tooltips" proof-output-tooltips-toggle :style toggle :selected proof-output-tooltips @@ -2563,6 +2563,70 @@ Warning: this makes the error messages (and location) wrong.") "Return t if the last tactic of locked region contains an \"as\" close." (save-excursion (string-match "\\<as\\>" s))) +;::::::::::::: inserting suggested Proof using XXX... ;;;;;;;;;; + +(defcustom accept-proof-using-suggestion 'ask + "Wether proofgeneral should automatically update proof using when +recieving suggestions from coq at Qed time." + :type '(choice + (const :tag "Ask user" ask) + (const :tag "always accept" always) + (const :tag "never accept" never)) + :group 'coq) + +(defun coq-extract-proof-using-from-suggestion () + (proof-with-current-buffer-if-exists proof-response-buffer + (when (string-match + "following commands:\n.*Proof using\\([^.]*\\)\\." + (buffer-string)) + (let* ((s (match-string 1 (buffer-string))) + (prefix (if (equal (aref s 0) ? ) " using" " using "))) + (concat prefix s))))) + +(defun coq-proof-using-equal (s1 s2) + (let* ((l1 (split-string s1)) (l2 (split-string s2)) + (diff (cl-set-exclusive-or l1 l2 :test 'string-equal))) + (not diff))) ;; nil if empty xor + + +(defun coq-insert-proof-using-suggestion (suggested) + ;; Not compatible with nested lemmas. + (with-current-buffer proof-script-buffer + (save-excursion + (goto-char (proof-unprocessed-begin)) + (let* ((pos-unproc (point)) + (proof-pos (save-excursion + (search-backward-regexp "\\<Proof\\>\\([^.]*\\)\\."))) + (previous-content (match-string 1)) + (same (coq-proof-using-equal previous-content suggested))) + (when (and (not same) (or (equal coq-accept-proof-using-suggestion 'always) + (y-or-n-p (concat "Update proof using annotation (" + suggested ")")))) + (goto-char (+ 5 proof-pos)) ; "Proof" has length 6 + ;(if (stored proof-strict-read-only) ) + (let ((spl proof-locked-span)) + ;; temporarily make the locked span writable + (span-read-write spl) + (delete-char (length previous-content)) + (insert suggested) + ;; go back to `proof-strict-read-only' says + (proof-span-read-only spl))))))) + +;; This should be called after a Save or Qed command is called (but not a +;; "Define"). +(defun coq-proof-using-suggest-hook () + (unless (equal coq-accept-proof-using-suggestion 'never) + (let ((suggestion (coq-extract-proof-using-from-suggestion))) + (when suggestion + (coq-insert-proof-using-suggestion suggestion))))) + + +(add-hook 'proof-shell-handle-delayed-output-hook + #'coq-proof-using-suggest-hook t) + + +;::::::::::::: inserting suggested Proof using XXX... ;;;;;;;;;; + (defun coq-insert-as-in-next-command () (interactive) |