From eb6bba151b27f4d821088e10e1bda5cad0b70a28 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 16 Oct 2020 16:33:34 +0200
Subject: Fix #518: "Proof using" mode corrupts "Proof with tac".

---
 coq/coq.el | 75 ++++++++++++++++++++++++++++++++++++++++++++++++--------------
 1 file changed, 58 insertions(+), 17 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 8cbf84a6..663279cf 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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.")
 
-- 
cgit v1.2.3