diff options
| -rw-r--r-- | coq/coq.el | 75 |
1 files changed, 58 insertions, 17 deletions
@@ -2621,9 +2621,28 @@ Warning: this makes the error messages (and location) wrong.") (save-excursion (string-match "\\<as\\>" s))) ;::::::::::::: inserting suggested Proof using XXX... ;;;;;;;;;; - +;; global mechanism: + +;; When some dependency oinformation is detected (see +;; `coq-shell-theorem-dependency-list-regexp') a hook is triggered by pg. We +;; configure this hook to perform the following: if the user set +;; `coq-accept-proof-using-suggestion' to 'always, then perform the insertion +;; immediately via using `coq-insert-proof-using', otherwise add the menu entry +;; to make it later (actually the current impolementation always adds the menu +;; entry, which is wrong because the span is not there if the insertion was +;; already performed.). + + +;; This variable is used by generic pg code. Every time this is detected in the +;; output, it sets the `proof-last-theorem-dependencies' variable. Substring 1 +;; should contain the name of the theorem, and substring 2 should contain its +;; dependencies. The content of `proof-last-theorem-dependencies' is then used +;; by pg generic code to trigger `proof-depends-process-dependencies', which +;; itself sets the 'dependencies property of the span, and calls +;; `proof-dependencies-system-specific'. The latter is bound to +;; `coq-dependencies-system-specific' below. (setq coq-shell-theorem-dependency-list-regexp - "<infomsg>\n?The proof of \\([^ \n]+\\)\\(?: \\|\n\\)should start with one of the following commands:\\(?: \\|\n\\)Proof using\\([^.]*\\)\\.") + "<infomsg>\n?The proof of \\(?1:[^ \n]+\\)\\(?: \\|\n\\)should start with one of the following commands:\\(?: \\|\n\\)Proof using\\(?2:[^.]*\\)\\.") (defcustom coq-accept-proof-using-suggestion 'highlight "Whether and how proofgeneral should insert \"Proof using\" suggestions. @@ -2662,6 +2681,12 @@ Remarks and limitations: (const :tag "Ignore completely" ignore)) :group 'coq) +;; putting "Type" instead of nothing, otherwise Coq may fail if a "with" +;; anotation is also present: (Proof using with auto raises an error in +;; coq<=8.12 at least). +(defun coq-hack-proofusing-suggestion (suggested) + (if (string-equal "" suggested) "Type" suggested)) + ;; the additional menu for "proof using". highlights the "Proof." command, and ;; have a entry to insert the annotation and remove the highlight. (defvar coq-dependency-menu-system-specific @@ -2669,20 +2694,31 @@ Remarks and limitations: (let* ((deps (span-property-safe span 'dependencies)) (specialspans (spans-at-region-prop (span-start span) (span-end span) 'proofusing)) (specialspan (and specialspans (not (cdr specialspans)) (car specialspans))) - (name (concat " insert \"proof using " (mapconcat 'identity deps " ") "\"")) + (suggested (mapconcat 'identity deps " ")) + (suggested (coq-hack-proofusing-suggestion suggested)) + (name (concat " insert \"proof using " suggested "\"")) (fn `(lambda (sp) (coq-insert-proof-using-suggestion sp t) - (span-delete ,specialspan)))) + (and ,specialspan (span-delete ,specialspan))))) (list "-------------" (vector name `(,fn ,span) t)))) "Coq specific additional menu entry for \"Proof using\". annotation. See `proof-dependency-menu-system-specific'." ) -(defconst coq-proof-using-regexp "\\_<Proof\\(?:\\s-+using\\>\\)?\\([^.]*\\)\\." - "regexp matching Coq \"Proof( using xxx)?.\" annotation. -There should be one subexp numbered 1 matching xxx if present.") +(defconst coq-proof-using-regexp "\\_<Proof\\(?1:[^.]*\\)\\." + "Regexp matching Coq \"Proof ....\" annotation (with no \"using\" annotation). +We suppose there is no \"using\" annotation, since Coq will fail +in this case and no suggestion can be added without replaying the +script. Actually the only possible content iafter Proof is a +\"with annotation\". +The substring matched numbered 1 must start at the possible +insertion point for the \"using\" annotation. ") -(defun coq-mark-span-dependencies (span suggested) + +;; span is typically the whole theorem statement+proof span built after a save +;; command +(defun coq-highlight-span-dependencies (span suggested) (goto-char (span-start span)) + ; Search for the "Proof" command and build a hilighted span on it (let* ((endpos (re-search-forward coq-proof-using-regexp)) (proof-pos (match-beginning 0)) (newspan (span-make proof-pos endpos))) @@ -2690,11 +2726,10 @@ There should be one subexp numbered 1 matching xxx if present.") (span-set-property newspan 'help-echo "Right click to insert \"proof using\"") (span-set-property newspan 'proofusing t))) -(defun coq-insert-proof-using (proof-pos previous-content string-suggested) - (goto-char (+ 5 proof-pos)) ; "Proof" has length 6 +(defun coq-insert-proof-using (proof-pos previous-content insert-point string-suggested) + (goto-char insert-point) (let ((spl proof-locked-span)) (span-read-write spl) ; temporarily make the locked span writable - (when previous-content (delete-char (length previous-content))) (insert (concat " using " string-suggested)) (proof-span-read-only spl))) @@ -2712,7 +2747,8 @@ There should be one subexp numbered 1 matching xxx if present.") (defun coq-insert-proof-using-suggestion (span &optional force) "Add the proof using annotation, respecting `coq-accept-proof-using-suggestion'. Insert \" using xxx\" After the \"Proof\" of SPAN, where xxx is -built from the list of strings in SUGGESTED." +built from the list of strings in SUGGESTED. +SPAN is the span of the whole theorem (statement + proof)." (with-current-buffer proof-script-buffer (save-excursion (goto-char (span-start span)) @@ -2720,9 +2756,13 @@ built from the list of strings in SUGGESTED." (when endpos (let* ((suggested (span-property span 'dependencies)) (proof-pos (match-beginning 0)) - (previous-content (split-string (match-string 1))) + (insert-point (match-beginning 1)) + (previous-string (match-string 1)) + (previous-content (split-string previous-string)) (string-suggested (mapconcat 'identity suggested " ")) - (same (and previous-content + (string-suggested (coq-hack-proofusing-suggestion string-suggested)) + ;; disabled for now it never happens because Coq would suggest anything? + (same (and nil previous-content (not (cl-set-exclusive-or previous-content suggested :test 'string-equal)))) (usersayyes @@ -2732,13 +2772,14 @@ built from the list of strings in SUGGESTED." string-suggested ")"))))) (unless same (if (or force (equal coq-accept-proof-using-suggestion 'always) usersayyes) - (coq-insert-proof-using proof-pos previous-content string-suggested) + (coq-insert-proof-using proof-pos previous-content insert-point string-suggested) (when (member coq-accept-proof-using-suggestion '(highlight ask)) - (coq-mark-span-dependencies span suggested) + (coq-highlight-span-dependencies span string-suggested) (message "\"Proof using\" not set. M-x coq-insert-suggested-dependency or right click to add it. See also `coq-accept-proof-using-suggestion'.")))))))))) (defvar coq-dependencies-system-specific - (lambda (span) (coq-insert-proof-using-suggestion span)) + (lambda (span) + (coq-insert-proof-using-suggestion span)) "Coq specific dependency mechanism. Used for automatic insertion of \"Proof using\" annotations.") |