fix issue #605

ProofGeneral · Mar 31, 2024 · 6feb2b1 · 6feb2b1
1 parent ceef0e4
commit 6feb2b1
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 5 deletions.
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
@@ -155,9 +155,6 @@ so the response buffer should not be cleared."
   ;; window.  Indicate it should be erased before the next output.
   (pg-response-maybe-erase t t nil keepresponse)
 
-  ;; ;; commit modif
-  ;; (reset-goals-modeline)
-
   ;; Erase the goals buffer and add in the new string
   (with-current-buffer proof-goals-buffer
 

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
@@ -870,7 +870,7 @@ after a completed proof."
     (proof-shell-exec-loop))
 
    ((proof-re-search-forward-safe proof-shell-proof-completed-regexp end t)
-    (setq proof-shell-proof-completed 0)))
+    (setq proof-shell-proof-completed 0))) ; commands since complete
 
   ;; PG4.0 change: simplify and run earlier
   (if proof-shell-handle-output-system-specific
@@ -1788,7 +1788,7 @@ i.e., 'goals or 'response."
 			gmark))
 	    (rstart start)		 ; possible response before goals
 	    (gend   end)
-	    both)
+	    both)                        ; flag for response+goals
 
        (goto-char gstart)
        (while (re-search-forward proof-shell-start-goals-regexp end t)