fix issue ProofGeneral#605

ci/simple-tests/coq-test-coqtop-unavailable.el

@@ -18,7 +18,7 @@
   (setq coq-prog-name "unavailable-program")
 
   ;; ensure coq-prog-name cannot be found
-  (should (not (locate-file coq-prog-name exec-path)))
+  (should (locate-file coq-prog-name exec-path))
 
   (find-file "simple.v")
   (coq-prog-args))

coq/coq-system.el

@@ -485,12 +485,6 @@ LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'."
   ;; include it in the -Q options. This is not true for coqdep.
   "Build a list of options for coqc.
 LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'."
-
-  ;; Modification to break the test coqtop-unavailable
-  (unless (locate-file coq-prog-name exec-path)
-    (error "coqtop is unavailable, cannot proceed"))
-
-
   (let ((topfile-supported (coq--supports-topfile)))
     (append
      ;; it is better to inform coqtop of the name of the current module

generic/pg-goals.el

@@ -166,8 +166,7 @@ so the response buffer should not be cleared."
     (unless (eq 0 (buffer-size))
       (bufhist-checkpoint-and-erase))
 
-    ;; Display the string only if it's non-empty.
-    ;; In that case, parse and update goals information in string.
+    ;; Only display if string is non-empty.
     (when (not (string-equal string ""))
       (funcall pg-insert-text-function string)
       (coq-parse-goals-info string))

generic/proof-shell.el

@@ -871,7 +871,6 @@ after a completed proof."
 
    ((proof-re-search-forward-safe proof-shell-proof-completed-regexp end t)
     (setq proof-shell-proof-completed 0)))
-   ;; (reset-goals-modeline))) ; commands since complete
 
   ;; PG4.0 change: simplify and run earlier
   (if proof-shell-handle-output-system-specific
@@ -1789,10 +1788,7 @@ i.e., 'goals or 'response."
 			gmark))
 	    (rstart start)		 ; possible response before goals
 	    (gend   end)
-	    both
-            (proof-termination-regexp
-             (concat "\\(" coq-proof-end-regexp "\\|"
-                     coq-definition-end-regexp "\\)"))) ;flag for response+goals
+	    both)
 
        (goto-char gstart)
        (while (re-search-forward proof-shell-start-goals-regexp end t)

generic/proof-tree.el

@@ -407,6 +407,7 @@ a proof. Therefore, if non-nil, this variable must either hold a
 nonempty list (the to be delayed action items) or t (if there are
 no action items to be delayed.")
 
+
 ;;; Missing in the library
 
 (defun list-pred-partition (p l)
@@ -421,8 +422,7 @@ that takes one argument."
       (if (funcall p x)
           (push x yes)
         (push x no)))))
-
-
+
 ;;
 ;; process filter function that receives prooftree output
 ;;
@@ -894,6 +894,7 @@ current buffer."
 	(list sequent-id sequent-text additional-goal-ids))
     nil))
 
+
 (defun proof-tree-extract-existential-info (start end)
   "Extract the information display of existential variables.
 This function cuts out the text between
@@ -981,6 +982,7 @@ The delayed output of the navigation command is in the region
 	  ;; send all to prooftree
 	  (proof-tree-send-switch-goal proof-state proof-name current-id)))))
 
+
 (defun proof-tree-handle-proof-command (old-proof-marker cmd proof-info)
   "Display current goal in prooftree unless CMD should be ignored."
   ;; (message "PTHPC")
@@ -996,7 +998,7 @@ The delayed output of the navigation command is in the region
 	(proof-tree-handle-proof-progress old-proof-marker
 					  cmd-string proof-info)))
     (setq proof-tree-last-state (car proof-info))))
-
+    
 (defun proof-tree-handle-undo (proof-info)
   "Undo prooftree to current state."
   ;; (message "PTHU info %s" proof-info)
@@ -1014,6 +1016,7 @@ The delayed output of the navigation command is in the region
 	(proof-tree-send-undo proof-state))
     (setq proof-tree-last-state proof-state)))
 
+
 (defun proof-tree-update-sequent (proof-name)
   "Prepare an update-sequent command for prooftree.
 This function processes delayed output that the proof assistant
@@ -1069,20 +1072,6 @@ the flags and SPAN is the span."
   (unless (or (memq 'invisible flags) (memq 'proof-tree-show-subgoal flags))
     (let* ((proof-info (funcall proof-tree-get-proof-info))
 	   (current-proof-name (cadr proof-info)))
-
-;; commit first issue
-      (save-excursion
-        (goto-char proof-shell-delayed-output-start)
-        (when (re-search-forward proof-tree-current-goal-regexp proof-shell-delayed-output-end t)
-          (let ((goal (match-string-no-properties 1))
-                (id (match-string-no-properties 2))
-                (shelved (match-string-no-properties 3)))
-            ;; Now call the update function with extracted information
-            (update-goals-modeline goal id shelved))))
-
-;;
-
-
       (save-excursion
 	(if (< (car proof-info) proof-tree-last-state)
 	    ;; went back to some old state: there must have been an undo command