Fix compile errors, update tags

4 files changed, 16 insertions, 12 deletions

diff --git a/generic/pg-user.el b/generic/pg-user.el
index ac2a3210..425ccb73 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -26,8 +26,8 @@
   (require 'completion)		       ; loaded dynamically at runtime
   (defvar which-func-modes nil))       ; defined by which-func
 
-; defined in proof-script/proof-setup-parsing-mechanism
 (declare-function proof-segment-up-to "proof-script") 
+(declare-function proof-interrupt-process "proof-shell") 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -1428,9 +1428,6 @@ assuming the undo-in-region behavior will apply if ARG is non-nil."
   "Adjust autosend timer when variable `proof-autosend-delay' changes."
   (proof-autosend-enable t))
 
-(defvar proof-autosend-running nil
-  "Flag indicating we are sending commands to the prover automatically.")
-
 (defun proof-autosend-loop ()
   (proof-with-current-buffer-if-exists proof-script-buffer
     (unless (proof-locked-region-full-p)
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index 1f22c629..cc788ca8 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -220,6 +220,11 @@ in `proof-shell-clear-state'.")
   "Contains the dependencies of the last theorem.  A list of strings.
 Set in `proof-shell-process-urgent-message'.")
 
+(defvar proof-autosend-running nil
+  "Flag indicating we are sending commands to the prover automatically.
+Used in `proof-autosend-loop' and inspected in other places to inhibit
+user interaction.")
+
 
 ;;
 ;; Not variables at all: global constants (were in proof-config)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index be2b84ca..25c87e10 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -31,6 +31,7 @@
 		  (string &optional push))
 (declare-function pg-response-warning "pg-response" (&rest args))
 (declare-function proof-segment-up-to "proof-script")
+(declare-function proof-autosend-enable "pg-user")
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index d99e2b67..238ba47b 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -54,6 +54,13 @@ If flags are non-empty, other interactive cues will be surpressed.
 
 See the functions `proof-start-queue' and `proof-shell-exec-loop'.")
 
+(defsubst proof-shell-invoke-callback (listitem)
+  "From `proof-action-list' LISTITEM, invoke the callback on the span."
+  (condition-case nil
+      (funcall (nth 2 listitem) (car listitem))
+    (error nil)))
+
+
 ;; We record the last output from the prover and a flag indicating its
 ;; type, as well as a previous ("delayed") version for when the end
 ;; of the queue is reached or an error or interrupt occurs.
@@ -644,12 +651,12 @@ This is a subroutine of `proof-shell-handle-error-or-interrupt'"
       (proof-script-clear-queue-spans-on-error badspan))
 
     (setq proof-action-list nil)
-    (proof-release-lock))
+    (proof-release-lock)
     ;; Give a hint about C-c C-`.  (NB: approximate test)
     (unless flags
       (if (pg-response-has-error-location)
 	  (pg-next-error-hint)))
-    (run-hooks 'proof-shell-handle-error-or-interrupt-hook)))
+    (run-hooks 'proof-shell-handle-error-or-interrupt-hook))))
 
 (defun proof-goals-pos (span maparg)
   "Given a span, return the start of it if corresponds to a goal, nil otherwise."
@@ -879,12 +886,6 @@ track what happens in the proof queue."
 	  (>= (length proof-action-list) proof-shell-silent-threshold)))
 
 
-(defsubst proof-shell-invoke-callback (listitem)
-  "From `proof-action-list' LISTITEM, invoke the callback on the span."
-  (condition-case nil
-      (funcall (nth 2 listitem) (car listitem))
-    (error nil)))
-
 (defsubst proof-shell-insert-action-item (item)
   "Insert ITEM from `proof-action-list' into the proof shell."
   (proof-shell-insert (nth 1 item) (nth 2 item) (nth 0 item)))