Add option to consider error message feedbacks as failures (& Fix retract bugs)

coq/coq-response.el

@@ -214,9 +214,10 @@ Only when three-buffer-mode is enabled."
 	      (span-set-property error-span 'help-echo msg)
 	      ;; must set priority using special call
 	      (span-set-priority error-span (gethash face coq-face-rank-tbl))
-	      (span-set-property error-span 'type 'pg-error)
-	      (when warp
-		(goto-char (+ start start-offs)))))))
+	      (span-set-property error-span 'type 'pg-error)))
+	  ;; warp even in the case of a duplicate
+	  (when warp
+	    (goto-char (+ start start-offs)))))
       ;; return start of error highlighting
       start)))
 

coq/coq-span.el

@@ -35,23 +35,23 @@
 (require 'coq-xml)
 (require 'coq-header-line)
 
-(defun coq-server--state-id-precedes (state-id-1 state-id-2)
+(defun coq-span-state-id-precedes (state-id-1 state-id-2)
   "Does STATE-ID-1 occur in a span before that for STATE-ID-2?"
-  (let ((span1 (coq-server--get-span-with-state-id state-id-1))
-	(span2 (coq-server--get-span-with-state-id state-id-2)))
+  (let ((span1 (coq-span-get-span-with-state-id state-id-1))
+	(span2 (coq-span-get-span-with-state-id state-id-2)))
     (< (span-start span1) (span-start span2))))
 
-(defun coq-server--get-span-with-predicate (pred &optional span-list)
+(defun coq-span-get-span-with-predicate (pred &optional span-list)
   (with-current-buffer proof-script-buffer
     (let* ((all-spans (or span-list (spans-all))))
       (cl-find-if pred all-spans))))
 
 ;; we could use the predicate mechanism, but this happens a lot
 ;; so use hash table
-(defun coq-server--get-span-with-state-id (state-id)
+(defun coq-span-get-span-with-state-id (state-id)
   (gethash state-id coq-span-state-id-tbl))
 
-(defun coq-server--get-span-with-edit-id (edit-id)
+(defun coq-span-get-span-with-edit-id (edit-id)
   (gethash edit-id coq-span-edit-id-tbl))
 
 (defun coq-span-color-span (span face)
@@ -63,7 +63,7 @@
 
 (defun coq-span-color-span-on-feedback (xml status face &optional force-processed)
   (let* ((state-id (coq-xml-at-path xml '(feedback (state_id val))))
-	 (span-with-state-id (coq-server--get-span-with-state-id state-id)))
+	 (span-with-state-id (coq-span-get-span-with-state-id state-id)))
     ;; can see feedbacks with state id not yet associated with a span
     ;; also can find a span with a state id that's been deleted from script buffer,
     ;;  but not yet garbage-collected from table

coq/coq-state-vars.el

@@ -79,14 +79,18 @@ It's the state id returned after Init command sent.")
 ;; values are weak, because spans can be deleted, as on a retract
 (defvar coq-span-state-id-tbl (make-hash-table :test 'equal :weakness 'key-and-value))
 
+;; table mapping spans to state id at time of an Add
+(defvar coq-span-add-state-id-tbl (make-hash-table :test 'equal :weakness 'key-and-value))
+
+;; table mapping state id at time of an Add to spans
+(defvar coq-add-state-id-span-tbl (make-hash-table :test 'equal :weakness 'key-and-value))
+
 ;; associate edit ids with spans
 ;; edit ids are numbers, so don't need to use 'equal as test like we did for state ids
 (defvar coq-span-edit-id-tbl (make-hash-table :weakness 'value))
 
-;; associate state ids with spans
-;; for a span, this is the state id in the corresponding Add call, NOT the state id later associated
-;;  with the span
-(defvar coq-span-add-call-state-id-tbl (make-hash-table :test 'equal :weakness 'key-and-value))
+;; associate edit ids with state-ids
+(defvar coq-edit-id-state-id-tbl (make-hash-table :weakness 'value))
 
 ;; table maps PG face to a rank governing precedence
 (defvar coq-face-rank-tbl (make-hash-table))
@@ -101,8 +105,10 @@ It's the state id returned after Init command sent.")
   (mapc 'clrhash
 	(list coq-error-fail-tbl
 	      coq-span-state-id-tbl
+	      coq-span-add-state-id-tbl
+	      coq-add-state-id-span-tbl
 	      coq-span-edit-id-tbl
-	      coq-span-add-call-state-id-tbl
+	      coq-edit-id-state-id-tbl
 	      coq-feedbacks-tbl)))
 
 (add-hook 'proof-server-restart-hook 'coq-reset-tables)

coq/coq-system.el

@@ -119,6 +119,11 @@ processes. By default, not enabled for Windows, for stability reasons."
   :type 'integer
   :group 'coq)
 
+(defcustom coq-errormsg-as-failure nil
+  "Error message feedbacks cause retraction"
+  :type 'boolean
+  :group 'coq)
+
 (defcustom coq-tags (concat coq-library-directory "/theories/TAGS")
   "The default TAGS table for the Coq library."
   :type 'string

coq/coq-tq.el

@@ -75,12 +75,14 @@
 	      last-search-point
 	      response-complete
 	      call
-	      span)
+	      span
+	      edit-id)
 
 (defun coq-tq-set-last-search-point (tq pt) (setf (coq-tq-last-search-point tq) pt))
 (defun coq-tq-set-queue             (tq queue) (setf (coq-tq-queue tq) queue))
 (defun coq-tq-set-call              (tq call) (setf (coq-tq-call tq) call))
 (defun coq-tq-set-span              (tq span) (setf (coq-tq-span tq) span))
+(defun coq-tq-set-edit-id           (tq edit-id) (setf (coq-tq-edit-id tq) edit-id))
 (defun coq-tq-set-complete          (tq) (setf (coq-tq-response-complete tq) t))
 (defun coq-tq-set-incomplete        (tq) (setf (coq-tq-response-complete tq) nil))
 
@@ -135,13 +137,16 @@
     ;; span will be non-nil for an Add
     (when span
       (coq-tq-set-span tq span))
+    ;; set edit id to return upon response
+    (coq-tq-set-edit-id tq coq-edit-id-counter)
     ;; update sent region
     ;; associate edit id with this span
     (when span
       (with-current-buffer proof-script-buffer
 	(coq-span-color-sent-span span)
 	(proof-set-sent-end (span-end span)))
-      (puthash coq-current-state-id span coq-span-add-call-state-id-tbl)
+      (puthash span coq-current-state-id coq-span-add-state-id-tbl)
+      (puthash coq-current-state-id span coq-add-state-id-span-tbl)
       (puthash coq-edit-id-counter span coq-span-edit-id-tbl))
     (process-send-string (coq-tq-process tq) str)))
 
@@ -294,7 +299,8 @@ needs, and the answer to the question."
 				   (coq-tq-queue-head-closure tq)
 				   answer
 				   (coq-tq-call tq)
-				   (coq-tq-span tq)))
+				   (coq-tq-span tq)
+				   (coq-tq-edit-id tq)))
 		      (error (proof-debug-message
 			      (concat "Error when processing "
 				      (if complete "complete" "partial")

coq/coq.el

@@ -525,12 +525,12 @@ nearest preceding span with a state id."
                (lambda (sp) (span-property sp 'processing-in))
                spans)))
         (mapc 'span-delete processing-spans)))
-    ;; if auto-retracting on error, leave error in response buffer
-    (if (or coq-server-retraction-on-error
-            coq-server-retraction-on-interrupt)
-        (setq coq-server-retraction-on-error nil
-              coq-server-retraction-on-interrupt nil)
+    ;; if auto-retracting on error or interrupt, leave error in response buffer
+    (unless (or coq-server-retraction-on-error
+                coq-server-retraction-on-interrupt)
       (coq-response-clear-response-buffer))
+    (when coq-server-retraction-on-interrupt
+      (setq coq-server-retraction-on-interrupt nil))
     ;; use nearest state id before this span; if none, retract buffer
     (if (and (= (span-start span) 1) coq-retract-buffer-state-id)
         (coq-server--send-retraction coq-retract-buffer-state-id t)
@@ -1131,7 +1131,7 @@ Near here means PT is either inside or just aside of a comment."
                     (signal-process pid 'SIGINT))
                   coq-pids)
             (setq coq-server-retraction-on-interrupt t))))
-      (let* ((current-span (coq-server--get-span-with-state-id coq-current-state-id))
+      (let* ((current-span (coq-span-get-span-with-state-id coq-current-state-id))
              (end (if current-span (span-end current-span) 1)))
         (proof-set-queue-end end)
         (proof-set-locked-end end))