diff --git a/generic/proof-config.el b/generic/proof-config.el
index 9632a2685..4f9dcfeac 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1464,7 +1464,15 @@ outside of any proof.
   :type 'function
   :group 'proof-script)
 
+(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.
 
+nil disables the timeout timer.
+
+Default value is 30 (seconds)."
+  :type 'integer
+  :group 'proof-shell)
 
 ;;
 ;; 3c. tokens mode: turning on/off tokens output
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index e39837c04..cf509378c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -149,6 +149,13 @@ 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 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.")
 
 
 ;;
@@ -738,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)
@@ -916,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)
 
@@ -1020,7 +1045,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
@@ -1188,7 +1212,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))
+	  (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))))))