From 1f2120a006f50c8512701ba7c030a8a74d5c3c4c Mon Sep 17 00:00:00 2001
From: ibynx <36119601+ibynx@users.noreply.github.com>
Date: Mon, 12 Oct 2020 10:18:29 -0400
Subject: [PATCH 01/11] Add proof-shell-timeout-warn variables (see #514)

---
 generic/proof-config.el | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 6f1e91487..7377f71d6 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1516,7 +1516,21 @@ outside of any proof.
   :type 'function
   :group 'proof-script)
 
+(defcustom proof-shell-timeout-warn-p t
+  "Whether Proof General should warn us if a command is taking
+too long and might be malformed.
 
+Set to nil to disable."
+  :type 'boolean
+  :group 'proof-shell)
+
+(defcustom proof-shell-timeout-warn-length 30
+  "If `proof-shell-timeout-p' is true, this tells PG how long to
+wait before warning the user, in seconds.
+
+Default value is 30 seconds. Set it as an integer."
+  :type 'integer
+  :group 'proof-shell)
 
 ;;
 ;; 3c. tokens mode: turning on/off tokens output

From 99cd00c91fe16a2fdcaf94abe2cd86ef9bc8abe8 Mon Sep 17 00:00:00 2001
From: ibynx <36119601+ibynx@users.noreply.github.com>
Date: Mon, 12 Oct 2020 10:19:44 -0400
Subject: [PATCH 02/11] Add shell-internal variable for timer (see #514)

---
 generic/proof-shell.el | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index af9b50e0f..4770e469c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -149,6 +149,12 @@ This flag is set for the duration of `proof-shell-kill-function'
 to tell hooks in `proof-deactivate-scripting-hook' to refrain
 from calling `proof-shell-exit'.")
 
+(defvar proof-shell-timer nil
+  "A timer that alerts the user when the current command sent to the
+shell is taking too long and might be malformed. This is reset on entry
+of `proof-shell-exec-loop' and set when the next command is sent to
+the process. Disable by setting `proof-shell-timeout-p' to nil.
+Configure with `proof-shell-timeout-length'")
 
 
 ;;
@@ -1176,8 +1182,8 @@ contains only invisible elements for Prooftree synchronization."
 	  (proof-shell-handle-error-or-interrupt 'interrupt flags))
 
 	(if proof-action-list
-	    ;; send the next command to the process.
-	    (proof-shell-insert-action-item (car proof-action-list)))
+	  ;; send the next command to the process.
+	  (proof-shell-insert-action-item (car proof-action-list)))
 
 	;; process the delayed callbacks now
 	(mapc 'proof-shell-invoke-callback cbitems)

From d8d61044fb2329dd5f812e633170d6c52a6e6519 Mon Sep 17 00:00:00 2001
From: ibynx <36119601+ibynx@users.noreply.github.com>
Date: Mon, 12 Oct 2020 13:53:05 -0400
Subject: [PATCH 03/11] Implement timeout message (see #514)

---
 generic/proof-script.el | 10 +++++++++-
 generic/proof-shell.el  |  8 +++++++-
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/generic/proof-script.el b/generic/proof-script.el
index a5109be7c..b3ae85229 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2025,7 +2025,15 @@ This function expects the buffer to be activated for advancing."
 	(lastpos   (nth 2 (car semis)))
 	(vanillas  (proof-semis-to-vanillas semis displayflags)))
     (proof-script-delete-secondary-spans startpos lastpos)
-    (proof-extend-queue lastpos vanillas)))
+    (proof-extend-queue lastpos vanillas))
+
+  ;; arm the timeout timer
+  ;; cancelled in proof-shell-exec-loop unless proof-shell-busy
+  (if proof-shell-timeout-warn-p
+      (setq proof-shell-timer
+          (run-with-timer proof-shell-timeout-warn-length nil
+                          'message "This command is taking a while. \
+Is it malformed? Do C-c C-c or C-c C-x to abort."))))
 
 (defun proof-retract-before-change (beg end)
   "For `before-change-functions'.  Retract to BEG unless BEG and END in comment.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 4770e469c..557c780a4 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1205,7 +1205,13 @@ contains only invisible elements for Prooftree synchronization."
 	 	   ;; If the last command in proof-action-list is a "Show Proof" form then return t
 	 	   (when last-command
              (proof-shell-string-match-safe
-              proof-show-proof-diffs-regexp last-command)))))))))
+              proof-show-proof-diffs-regexp last-command))))))))
+
+	(unless proof-shell-busy
+		;; if the shell isn't still busy, cancel timer
+		(if (and proof-shell-timer proof-shell-timeout-p)
+			(progn (cancel-timer proof-shell-timer)
+			       (setq proof-shell-timer nil)))
 
 
 (defun proof-shell-insert-loopback-cmd  (cmd)

From ebea62f0ed62d946b3b7b8a67a17659f094341f7 Mon Sep 17 00:00:00 2001
From: ibynx <36119601+ibynx@users.noreply.github.com>
Date: Mon, 12 Oct 2020 18:11:12 -0400
Subject: [PATCH 04/11] fix parentheses

---
 generic/proof-shell.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 557c780a4..7ec7466ef 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1211,7 +1211,7 @@ contains only invisible elements for Prooftree synchronization."
 		;; if the shell isn't still busy, cancel timer
 		(if (and proof-shell-timer proof-shell-timeout-p)
 			(progn (cancel-timer proof-shell-timer)
-			       (setq proof-shell-timer nil)))
+			       (setq proof-shell-timer nil)))))
 
 
 (defun proof-shell-insert-loopback-cmd  (cmd)

From 3ab615957b539581501a5f5c948982eeede9f3a9 Mon Sep 17 00:00:00 2001
From: ibynx <36119601+ibynx@users.noreply.github.com>
Date: Mon, 12 Oct 2020 18:43:12 -0400
Subject: [PATCH 05/11] fix empty goals bug because of previous commit
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The previous commits’ proof-shell.el had the timeout cancel in the
wrong place, leading to a bug with an empty buffer.
---
 generic/proof-shell.el | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 7ec7466ef..14de43bfb 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1196,6 +1196,12 @@ contains only invisible elements for Prooftree synchronization."
 	    (pg-processing-complete-hint))
 	  (pg-finish-tracing-display))
 
+  (unless proof-shell-busy
+		;; if the shell isn't still busy, cancel timer
+		(if (and proof-shell-timer proof-shell-timeout-warn-p)
+			(progn (cancel-timer proof-shell-timer)
+			       (setq proof-shell-timer nil))))
+
 	(and (not proof-second-action-list-active) 
 	     (let ((last-command  (car (nth 1 (car (last proof-action-list))))))
 	       (or (null proof-action-list)
@@ -1205,13 +1211,7 @@ contains only invisible elements for Prooftree synchronization."
 	 	   ;; If the last command in proof-action-list is a "Show Proof" form then return t
 	 	   (when last-command
              (proof-shell-string-match-safe
-              proof-show-proof-diffs-regexp last-command))))))))
-
-	(unless proof-shell-busy
-		;; if the shell isn't still busy, cancel timer
-		(if (and proof-shell-timer proof-shell-timeout-p)
-			(progn (cancel-timer proof-shell-timer)
-			       (setq proof-shell-timer nil)))))
+              proof-show-proof-diffs-regexp last-command)))))))))
 
 
 (defun proof-shell-insert-loopback-cmd  (cmd)

From 9a388528e637be103711b28ab972ea54cdbe050c Mon Sep 17 00:00:00 2001
From: ibynx <36119601+ibynx@users.noreply.github.com>
Date: Mon, 12 Oct 2020 19:38:46 -0400
Subject: [PATCH 06/11] change timer config to one variable

also minor whitespace formatting to match with master
---
 generic/proof-config.el | 16 +++++-----------
 generic/proof-script.el |  4 ++--
 generic/proof-shell.el  |  8 ++++----
 3 files changed, 11 insertions(+), 17 deletions(-)

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 7377f71d6..3168c0252 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1516,19 +1516,13 @@ outside of any proof.
   :type 'function
   :group 'proof-script)
 
-(defcustom proof-shell-timeout-warn-p t
-  "Whether Proof General should warn us if a command is taking
-too long and might be malformed.
+(defcustom proof-shell-timeout-warn 30
+  "How many seconds (integer) to wait before PG warns us that
+a command is taking a long time and might be malformed.
 
-Set to nil to disable."
-  :type 'boolean
-  :group 'proof-shell)
-
-(defcustom proof-shell-timeout-warn-length 30
-  "If `proof-shell-timeout-p' is true, this tells PG how long to
-wait before warning the user, in seconds.
+Nil disables the timeout timer.
 
-Default value is 30 seconds. Set it as an integer."
+Default value is 30 (seconds)."
   :type 'integer
   :group 'proof-shell)
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index b3ae85229..92542b10a 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2029,9 +2029,9 @@ This function expects the buffer to be activated for advancing."
 
   ;; arm the timeout timer
   ;; cancelled in proof-shell-exec-loop unless proof-shell-busy
-  (if proof-shell-timeout-warn-p
+  (if proof-shell-timeout-warn
       (setq proof-shell-timer
-          (run-with-timer proof-shell-timeout-warn-length nil
+          (run-with-timer proof-shell-timeout-warn nil
                           'message "This command is taking a while. \
 Is it malformed? Do C-c C-c or C-c C-x to abort."))))
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 14de43bfb..f06ffd182 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1181,9 +1181,9 @@ contains only invisible elements for Prooftree synchronization."
 	  (setq cbitems nil)
 	  (proof-shell-handle-error-or-interrupt 'interrupt flags))
 
-	(if proof-action-list
-	  ;; send the next command to the process.
-	  (proof-shell-insert-action-item (car proof-action-list)))
+  (if proof-action-list
+	    ;; send the next command to the process.
+	    (proof-shell-insert-action-item (car proof-action-list)))
 
 	;; process the delayed callbacks now
 	(mapc 'proof-shell-invoke-callback cbitems)
@@ -1198,7 +1198,7 @@ contains only invisible elements for Prooftree synchronization."
 
   (unless proof-shell-busy
 		;; if the shell isn't still busy, cancel timer
-		(if (and proof-shell-timer proof-shell-timeout-warn-p)
+		(if (and proof-shell-timer proof-shell-timeout-warn)
 			(progn (cancel-timer proof-shell-timer)
 			       (setq proof-shell-timer nil))))
 

From f8c0c09971d26c8edf5ae7ec1143a3c8536f9b76 Mon Sep 17 00:00:00 2001
From: ibynx <36119601+ibynx@users.noreply.github.com>
Date: Tue, 13 Oct 2020 09:39:41 -0400
Subject: [PATCH 07/11] Change warning text to clarify C-c C-c vs C-c C-x

---
 generic/proof-script.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 92542b10a..26768ac01 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2033,7 +2033,7 @@ This function expects the buffer to be activated for advancing."
       (setq proof-shell-timer
           (run-with-timer proof-shell-timeout-warn nil
                           'message "This command is taking a while. \
-Is it malformed? Do C-c C-c or C-c C-x to abort."))))
+Is it malformed? Do C-c C-c to interrupt prover or C-c C-x to terminate it."))))
 
 (defun proof-retract-before-change (beg end)
   "For `before-change-functions'.  Retract to BEG unless BEG and END in comment.

From 11d8c59a5da600a26cf7741d141c8bc15415ec6a Mon Sep 17 00:00:00 2001
From: ibynx <36119601+ibynx@users.noreply.github.com>
Date: Wed, 14 Oct 2020 09:57:11 -0400
Subject: [PATCH 08/11] cancel timer in the case of error or interrupt

also clarify documentation
---
 generic/proof-config.el |  2 +-
 generic/proof-script.el |  3 ++-
 generic/proof-shell.el  | 14 ++++++++++----
 3 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 3168c0252..80a9c8d5a 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1520,7 +1520,7 @@ outside of any proof.
   "How many seconds (integer) to wait before PG warns us that
 a command is taking a long time and might be malformed.
 
-Nil disables the timeout timer.
+nil disables the timeout timer.
 
 Default value is 30 (seconds)."
   :type 'integer
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 26768ac01..1151ed9cf 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2028,7 +2028,8 @@ This function expects the buffer to be activated for advancing."
     (proof-extend-queue lastpos vanillas))
 
   ;; arm the timeout timer
-  ;; cancelled in proof-shell-exec-loop unless proof-shell-busy
+  ;; cancelled 1. in `proof-shell-exec-loop' unless `proof-shell-busy' or
+  ;; 2. in the case of error, in `proof-shell-error-or-interrupt-action'
   (if proof-shell-timeout-warn
       (setq proof-shell-timer
           (run-with-timer proof-shell-timeout-warn nil
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index f06ffd182..7c8cf8369 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -151,10 +151,11 @@ from calling `proof-shell-exit'.")
 
 (defvar proof-shell-timer nil
   "A timer that alerts the user when the current command sent to the
-shell is taking too long and might be malformed. This is reset on entry
-of `proof-shell-exec-loop' and set when the next command is sent to
-the process. Disable by setting `proof-shell-timeout-p' to nil.
-Configure with `proof-shell-timeout-length'")
+shell is taking too long and might be malformed. This is cancelled
+in `proof-shell-exec-loop' or if there was an error and armed when
+the next command is sent to the process.
+Disable by setting `proof-shell-timeout-warn' to nil. Configure by
+setting `proof-shell-timeout-warn' to an integer.")
 
 
 ;;
@@ -744,6 +745,11 @@ unless the FLAGS for the command are non-nil (see `proof-action-list')."
     ;; proof-action-list is empty on error.
     (setq proof-action-list nil)
     (proof-release-lock)
+    (unless proof-shell-busy
+		;; if the shell isn't still busy, cancel timer on error
+      (if (and proof-shell-timer proof-shell-timeout-warn)
+          (progn (cancel-timer proof-shell-timer)
+                 (setq proof-shell-timer nil))))
     (unless flags
       ;; Give a hint about C-c C-`.  (NB: approximate test)
       (if (pg-response-has-error-location)

From ae1b7661628b633914026739c54ee15c45569b0f Mon Sep 17 00:00:00 2001
From: Andy Han <andyhan@mme-psychosis.cinci.rr.com>
Date: Sun, 21 Mar 2021 12:38:07 -0400
Subject: [PATCH 09/11] implement matafou's suggestions

---
 generic/proof-script.el | 9 ++++++---
 generic/proof-shell.el  | 2 +-
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 1151ed9cf..ed58f2045 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2030,11 +2030,14 @@ This function expects the buffer to be activated for advancing."
   ;; arm the timeout timer
   ;; cancelled 1. in `proof-shell-exec-loop' unless `proof-shell-busy' or
   ;; 2. in the case of error, in `proof-shell-error-or-interrupt-action'
-  (if proof-shell-timeout-warn
+  (if (and proof-shell-timeout-warn
+           (not (eq (caar semis) 'comment)))
       (setq proof-shell-timer
           (run-with-timer proof-shell-timeout-warn nil
-                          'message "This command is taking a while. \
-Is it malformed? Do C-c C-c to interrupt prover or C-c C-x to terminate it."))))
+                          'message
+                          (substitute-command-keys "This command is taking a while. \
+Is it malformed? Do \\[proof-interrupt-process] to interrupt prover or
+\\[proof-shell-exit] to terminate it.")))))
 
 (defun proof-retract-before-change (beg end)
   "For `before-change-functions'.  Retract to BEG unless BEG and END in comment.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 7c8cf8369..1d71be142 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1187,7 +1187,7 @@ contains only invisible elements for Prooftree synchronization."
 	  (setq cbitems nil)
 	  (proof-shell-handle-error-or-interrupt 'interrupt flags))
 
-  (if proof-action-list
+	(if proof-action-list
 	    ;; send the next command to the process.
 	    (proof-shell-insert-action-item (car proof-action-list)))
 

From debe754ecbc1fd6251ae2ae90d4eedc2c4627eba Mon Sep 17 00:00:00 2001
From: Andy Han <andyhan@mme-psychosis.cinci.rr.com>
Date: Sat, 27 Mar 2021 20:13:51 -0400
Subject: [PATCH 10/11] =?UTF-8?q?more=20fixes=E2=80=A6=20seems=20to=20work?=
 =?UTF-8?q?=20lol?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 generic/proof-script.el | 14 +-------------
 generic/proof-shell.el  | 27 ++++++++++++++++++---------
 2 files changed, 19 insertions(+), 22 deletions(-)

diff --git a/generic/proof-script.el b/generic/proof-script.el
index ae311823a..87a9975b7 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2011,19 +2011,7 @@ This function expects the buffer to be activated for advancing."
 	(lastpos   (nth 2 (car semis)))
 	(vanillas  (proof-semis-to-vanillas semis displayflags)))
     (proof-script-delete-secondary-spans startpos lastpos)
-    (proof-extend-queue lastpos vanillas))
-
-  ;; arm the timeout timer
-  ;; cancelled 1. in `proof-shell-exec-loop' unless `proof-shell-busy' or
-  ;; 2. in the case of error, in `proof-shell-error-or-interrupt-action'
-  (if (and proof-shell-timeout-warn
-           (not (eq (caar semis) 'comment)))
-      (setq proof-shell-timer
-          (run-with-timer proof-shell-timeout-warn nil
-                          'message
-                          (substitute-command-keys "This command is taking a while. \
-Is it malformed? Do \\[proof-interrupt-process] to interrupt prover or
-\\[proof-shell-exit] to terminate it.")))))
+    (proof-extend-queue lastpos vanillas)))
 
 (defun proof-retract-before-change (beg end)
   "For `before-change-functions'.  Retract to BEG unless BEG and END in comment.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index b50d9a40c..352be31c8 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1032,7 +1032,6 @@ being processed."
 	    "proof-append-alist: wrong queuemode detected for busy shell")
 	   (cl-assert (eq proof-shell-busy queuemode)))))
 
-
   (let ((nothingthere (null proof-action-list)))
     ;; Now extend or start the queue.
     (setq proof-action-list
@@ -1040,7 +1039,19 @@ being processed."
     
     (when nothingthere ; process comments immediately
       (let ((cbitems  (proof-shell-slurp-comments)))
-	(mapc 'proof-shell-invoke-callback cbitems)))
+	(mapc 'proof-shell-invoke-callback cbitems)
+	(when (and (< (length cbitems) (length proof-action-list))
+		   proof-shell-timeout-warn
+		   (not proof-shell-timer))
+	  ;; arm the timer if proof-action-list isn't just comments
+	  ;; cancelled 1. in `proof-shell-exec-loop' unless `proof-shell-busy' or
+	  ;; 2. in the case of error, in `proof-shell-error-or-interrupt-action'
+	  (setq proof-shell-timer
+		(run-with-timer proof-shell-timeout-warn nil
+				'message
+				(substitute-command-keys "This command is taking a while. \
+Is the syntax correct? Do \\[proof-interrupt-process] to interrupt prover or
+\\[proof-shell-exit] to terminate it."))))))
   
     (if proof-action-list ;; something to do
 	(progn
@@ -1200,13 +1211,11 @@ contains only invisible elements for Prooftree synchronization."
 	  (proof-detach-queue)
 	  (unless flags ; hint after a batch of scripting
 	    (pg-processing-complete-hint))
-	  (pg-finish-tracing-display))
-
-  (unless proof-shell-busy
-		;; if the shell isn't still busy, cancel timer
-		(if (and proof-shell-timer proof-shell-timeout-warn)
-			(progn (cancel-timer proof-shell-timer)
-			       (setq proof-shell-timer nil))))
+	  (pg-finish-tracing-display)
+	  (when (and proof-shell-timeout-warn proof-shell-timer)
+	    ;; cancel timer if there's nothing in the action lists
+	    (progn (cancel-timer proof-shell-timer)
+		   (setq proof-shell-timer nil))))
 
 	(and (not proof-second-action-list-active) 
 	     (let ((last-command  (car (nth 1 (car (last proof-action-list))))))

From 1cc7e70b19cf2967f0307f64ad6ed6bb428fa297 Mon Sep 17 00:00:00 2001
From: Andy Han <andyhan@mme-psychosis.cinci.rr.com>
Date: Sat, 3 Apr 2021 08:39:00 -0400
Subject: [PATCH 11/11] arm timer every command, not every region

---
 generic/proof-shell.el | 33 +++++++++++++++++----------------
 1 file changed, 17 insertions(+), 16 deletions(-)

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 352be31c8..cf509378c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -746,10 +746,10 @@ unless the FLAGS for the command are non-nil (see `proof-action-list')."
     (setq proof-action-list nil)
     (proof-release-lock)
     (unless proof-shell-busy
-		;; if the shell isn't still busy, cancel timer on error
+      ;; if the shell isn't still busy, cancel timer on error
       (if (and proof-shell-timer proof-shell-timeout-warn)
-          (progn (cancel-timer proof-shell-timer)
-                 (setq proof-shell-timer nil))))
+	  (progn (cancel-timer proof-shell-timer)
+		 (setq proof-shell-timer nil))))
     (unless flags
       ;; Give a hint about C-c C-`.  (NB: approximate test)
       (if (pg-response-has-error-location)
@@ -928,6 +928,19 @@ used in `proof-add-to-queue' when we start processing a queue, and in
       ;; Replace CRs from string with spaces to avoid spurious prompts.
       (if proof-shell-strip-crs-from-input
 	  (setq string (subst-char-in-string ?\n ?\  string)))
+      ;; arm the timer if we've received a user command (callback is proof-done-advancing)
+      (when (and (eq 'proof-done-advancing action)
+		 proof-shell-timeout-warn)
+	(when proof-shell-timer
+	  ;; cancel previous timer, if it exists
+	  (cancel-timer proof-shell-timer)
+	  (setq proof-shell-timer nil))
+	(setq proof-shell-timer
+	      (run-with-timer proof-shell-timeout-warn nil
+			      'message
+			      (substitute-command-keys "This command is taking a while. \
+Is the syntax correct? Do \\[proof-interrupt-process] to interrupt prover or
+\\[proof-shell-exit] to terminate it."))))
 
       (insert string)
 
@@ -1039,19 +1052,7 @@ being processed."
     
     (when nothingthere ; process comments immediately
       (let ((cbitems  (proof-shell-slurp-comments)))
-	(mapc 'proof-shell-invoke-callback cbitems)
-	(when (and (< (length cbitems) (length proof-action-list))
-		   proof-shell-timeout-warn
-		   (not proof-shell-timer))
-	  ;; arm the timer if proof-action-list isn't just comments
-	  ;; cancelled 1. in `proof-shell-exec-loop' unless `proof-shell-busy' or
-	  ;; 2. in the case of error, in `proof-shell-error-or-interrupt-action'
-	  (setq proof-shell-timer
-		(run-with-timer proof-shell-timeout-warn nil
-				'message
-				(substitute-command-keys "This command is taking a while. \
-Is the syntax correct? Do \\[proof-interrupt-process] to interrupt prover or
-\\[proof-shell-exit] to terminate it."))))))
+	(mapc 'proof-shell-invoke-callback cbitems)))
   
     (if proof-action-list ;; something to do
 	(progn