Reduce compiler warnings. Minor fixes.

21 files changed, 379 insertions, 179 deletions

diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index 9372d3d1..4eeff21c 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -34,6 +34,7 @@
 ;; Return a list of associated buffers
 ;;
 
+;;;###autoload
 (defun proof-associated-buffers ()
   "Return a list of the associated buffers.  
 Some may be dead/nil."
@@ -43,6 +44,7 @@ Some may be dead/nil."
 	proof-thms-buffer))
 
 
+;;;###autoload
 (defun proof-associated-windows ()
   "Return a list of the associated buffers windows.  
 Dead or nil buffers are not represented in the list."
diff --git a/generic/pg-pgip-old.el b/generic/pg-pgip-old.el
index 49287b7e..168cc86e 100644
--- a/generic/pg-pgip-old.el
+++ b/generic/pg-pgip-old.el
@@ -5,8 +5,9 @@
 ;; needed is for interim backward compatibility with Isabelle2003 and
 ;; Isabelle2004, for processing preference settings.
 ;;
+;; This will be removed in the next version of Proof General.
 
-;; FIXME: resurrect pg-prover-interpret-pgip-command (could try with pg-pgip-string-of-command)
+(require 'pg-xml)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; 
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index f2a8286e..9c8865da 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -30,6 +30,7 @@
 (require 'cl)				; incf
 (require 'pg-xml)
 (require 'pg-pgip-old)			;; Handle some PGIP 1.X format messages
+(require 'proof-config)			;; config variables
 
 ;;; Code:
 (defalias 'pg-pgip-debug   'proof-debug)
@@ -80,7 +81,7 @@ Return a symbol representing the PGIP command processed, or nil."
     (if (fboundp fname)
 	(progn
 	  (pg-pgip-debug "Processing PGIP message seq %s, type %s"
-			 (pg-xml-get-attr 'seq pgip 'notreallyoptional) name)
+			 (pg-xml-get-attr 'seq pgipmsg 'notreallyoptional) name)
 	  (funcall fname pgipmsg)
 	  name)
       (pg-internal-warning "!!! unrecognized/unimplemented PGIP message element `%s'" name)
@@ -113,8 +114,9 @@ Return a symbol representing the PGIP command processed, or nil."
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (defun pg-pgip-process-askpgip (node)
-  (pg-pgip-debug "Received <askpgip> message with version `%s'" version)
-  ;; FIXME: send a uses PGIP message back?
+  (pg-pgip-debug "Received <askpgip> message with version `%s'" 
+		 (pg-xml-get-attr 'version node 'notreallyoptional))
+  ;; TODO: send a uses PGIP message back?
   )
 
 (defun pg-pgip-process-usespgip (node)
diff --git a/generic/pg-response.el b/generic/pg-response.el
index ee5bb9ba..b34b6b7a 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -306,6 +306,7 @@ Returns non-nil if response buffer was cleared."
   
 ;; TODO: this function should be combined with
 ;; pg-response-maybe-erase-buffer.
+;;;###autoload
 (defun pg-response-display-with-face (str &optional face)
   "Display STR with FACE in response buffer."
   (cond
@@ -488,7 +489,7 @@ We fontify the output only if we're not too busy to do so."
       (newline))
     ;; If tracing output is prolific, we try to avoid
     ;; fontifying every chunk and batch it up instead.
-    (unless pg-tracing-slow-mode ; defined in proof-shell.el
+    (unless pg-tracing-slow-mode
       (let ((fontifystart (proof-trace-fontify-pos)))
 	;; Catch errors here: this is to deal with ugly problem when
 	;; fontification of large output gives error Nesting too deep
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 38217689..dee6922e 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -9,10 +9,19 @@
 ;;
 ;;; Commentary:
 ;; 
+;; This file defines some user-level commands.  Most of them
+;; are script-based operations.  Exported user-level commands
+;; are defined here as autoloads to avoid circular requires.
 
 ;;; Code:
 
-(require 'proof-utils)			; deflocal, proof-deftoggle
+(require 'span)
+(require 'proof)			; loader
+(require 'proof-script)			; we build on proof-script
+(require 'comint)			; comint-interrupt-subjob
+
+(eval-when-compile
+  (require 'completion))		; loaded dynamically at runtime
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -135,6 +144,7 @@ the proof script."
 ;; Interrupt
 ;;
 
+;;;###autoload
 (defun proof-interrupt-process ()
   "Interrupt the proof assistant.  Warning! This may confuse Proof General.
 This sends an interrupt signal to the proof assistant, if Proof General
@@ -225,6 +235,7 @@ handling of interrupt signals."
 ;; FIXME da: improvement would be to allow selection of part
 ;; of command by dragging, as in ordinary mouse-track-insert.
 ;; Maybe by setting some of the mouse track hooks.
+;; TODO: mouse-track-insert is XEmacs specific anyway.
 (defun proof-mouse-track-insert (event)
   "Copy highlighted command under the mouse to point.  Ignore comments.
 If there is no command under the mouse, behaves like mouse-track-insert."
@@ -251,7 +262,8 @@ If there is no command under the mouse, behaves like mouse-track-insert."
     ;; buffer, point position.
     (if str
 	(insert str proof-script-command-separator)
-      (mouse-track-insert event))))
+      (if (featurep 'xemacs)
+	  (mouse-track-insert event)))))
 
 
 
@@ -541,27 +553,22 @@ This is intended as a value for proof-activate-scripting-hook"
 
 ;; Register proof-electric-terminator as a minor mode.
 
-(deflocal proof-electric-terminator nil
-  "Fake minor mode for electric terminator.")
-
-(or (assq 'proof-electric-terminator minor-mode-alist)
+(or (assq 'proof-electric-terminator-enable minor-mode-alist)
     (setq minor-mode-alist
 	  (append minor-mode-alist
-		  (list '(proof-electric-terminator
+		  (list '(proof-electric-terminator-enable
 			  (concat " " proof-terminal-string))))))
 
-;; This is a value used by custom-set property = proof-set-value.
+;; This is a function called by custom-set property = proof-set-value.
+;;;###autoload
 (defun proof-electric-terminator-enable ()
-  "Copy proof-electric-terminator-enable to all script mode copies of it.
-Make sure the modeline is updated to display new value for electric terminator."
-  (if proof-mode-for-script
-      (proof-map-buffers (proof-buffers-in-mode proof-mode-for-script)
-			 (setq proof-electric-terminator
-			       proof-electric-terminator-enable)))
+  "Make sure the modeline is updated to display new value for electric terminator."
+  ;; TODO: probably even this isn't necessary
   (redraw-modeline))
 
 (proof-deftoggle proof-electric-terminator-enable proof-electric-terminator-toggle)
 
+;;;###autoload
 (defun proof-electric-term-incomment-fn ()
   "Used as argument to proof-assert-until-point."
   ;; CAREFUL: (1) dynamic scoping here  (incomment, ins, mrk)
@@ -685,7 +692,7 @@ last use time, to discourage saving these into the users database."
   (if proof-shell-last-output
       ;; There may be a system specific function to insert the comment
       (if pg-insert-output-as-comment-fn
-	  (pg-insert-output-as-comment-fn proof-shell-last-output)
+	  (funcall pg-insert-output-as-comment-fn proof-shell-last-output)
 	;; Otherwise the default behaviour is to use comment-region
 	(let  ((beg (point)) end)
 	  ;; pg-assoc-strip-subterm-markup: should be done
@@ -762,7 +769,7 @@ last use time, to discourage saving these into the users database."
 (defun pg-move-span-contents (span num)
   "Move SPAN up/downwards in the buffer, past NUM spans.
 If NUM is negative, move upwards.  Return new span."
-  ;; FIXME: maybe num arg is overkill, should only have 1?
+  ;; TODO: maybe num arg is overkill, should only have 1?
   (save-excursion
     (let  ((downflag (> num 0)) nextspan)
       ;; Always move a control span instead; it contains
@@ -777,7 +784,7 @@ If NUM is negative, move upwards.  Return new span."
       ;; When we delete the span, we want to duplicate it
       ;; to recreate in the new position.
       (span-set-property span 'duplicable 't)
-      ;; FIXME: this is faulty: moving span up gives children
+      ;; TODO: this is faulty: moving span up gives children
       ;; list with single nil element.  Hence liveness test
       (mapcar (lambda (s) (if (span-live-p s)
 			      (span-set-property s 'duplicable 't)))
@@ -792,7 +799,7 @@ If NUM is negative, move upwards.  Return new span."
 	     ;; lockedend doesn't move while in this code).
 	     (lockedend (span-end proof-locked-span)))
 	(let ((inhibit-read-only t))
-	  ;; FIXME: undo behaviour isn't quite right yet.
+	  ;; TODO: undo behaviour isn't quite right yet.
 	  (undo-boundary)
 	  (delete-region start end)
 	  (let ((insertpos (if downflag
@@ -804,21 +811,22 @@ If NUM is negative, move upwards.  Return new span."
 	    (insert contents)
 	    (let ((new-span
 		   (span-at insertpos 'type)));should be one we deleted.
-	      (span-set-property
-	       new-span 'children
-	       (append
-		(span-mapcar-spans 'pg-fixup-children-span
-			      insertpos (point) 'type)))
+	      (span-set-property new-span 'children
+				 (pg-fixup-children-spans 
+				  new-span insertpos (point)))
 	      (span-set-end proof-locked-span lockedend)
 	      (undo-boundary)
 	      new-span)))))))
 
-(defun pg-fixup-children-span (span)
-  (if (span-property span 'controlspan)
-      (progn
-	;; WARNING: dynamic binding for new-span
-	(span-set-property span 'controlspan new-span)
-	(list span))))
+(defun pg-fixup-children-spans (new-parent start end)
+  (append
+   (span-mapcar-spans 
+    (lambda (span)
+      (if (span-property span 'controlspan)
+	  (progn
+	    (span-set-property span 'controlspan new-parent)
+	    (list span))))
+    start end 'type)))
       
 (defun pg-move-region-down (&optional num)
   "Move the region under point downwards in the buffer, past NUM spans."
@@ -896,32 +904,27 @@ If NUM is negative, move upwards.  Return new span."
 ;; Span menus and keymaps  (maybe belongs in pg-menu)
 ;;
 
-(defvar pg-span-context-menu-keymap
-    (let ((map (make-sparse-keymap
-		"Keymap for context-sensitive menus on spans")))
-      (cond
-       ((featurep 'xemacs)
-	(define-key map [button3] 'pg-span-context-menu))
-       ((not (featurep 'xemacs))
-	(define-key map [down-mouse-3] 'pg-span-context-menu)))
-      map))
-
 ;; FIXME: TODO here:
 ;;
 ;; Check for a 'type which is one of the elements we know about
 ;; (pgidioms).
 ;;
 
-(defun pg-span-for-event (event)
-  "Return span corresponding to position of a mouse click EVENT."
+(defun pg-pos-for-event (event)
+  "Return position corresponding to position of a mouse click EVENT."
   (cond
    ((featurep 'xemacs)
-    (select-window (event-window event))
-    (span-at (event-point event) 'type))
-   ((not (featurep 'xemacs))
+    (when (event-window event)
+      (select-window (event-window event))
+      (event-point event)))
+   (t
     (with-current-buffer
 	(window-buffer (posn-window (event-start event)))
-      (span-at  (posn-point (event-start event)) 'type)))))
+      (posn-point (event-start event))))))
+
+(defun pg-span-for-event (event)
+  "Return span corresponding to position of a mouse click EVENT."
+  (span-at (pg-pos-for-event event) 'type))
 
 (defun pg-span-context-menu (event)
   (interactive "e")
@@ -1030,9 +1033,11 @@ If NUM is negative, move upwards.  Return new span."
 (defun pg-goals-buffers-hint ()
   (pg-hint "Use \\[proof-display-some-buffers] to rotate output buffers; \\[pg-response-clear-displays] to clear response & trace."))
 
+;;;###autoload
 (defun pg-slow-fontify-tracing-hint ()
   (pg-hint "Large tracing output; decorating intermittently.  Use \\[pg-response-clear-displays] to clear trace."))
 
+;;;###autoload
 (defun pg-response-buffers-hint (&optional nextbuf)
   (pg-hint
    (format
@@ -1042,9 +1047,11 @@ If NUM is negative, move upwards.  Return new span."
 		(if nextbuf (concat " (next:" nextbuf ")") ""))
       ""))))
 
+;;;###autoload
 (defun pg-jump-to-end-hint ()
   (pg-hint "Use \\[proof-goto-end-of-locked] to jump to end of processed region"))
   
+;;;###autoload
 (defun pg-processing-complete-hint ()
   "Display hint for showing end of locked region or processing complete."
   (if (buffer-live-p proof-script-buffer)
@@ -1061,10 +1068,12 @@ If NUM is negative, move upwards.  Return new span."
 	     (t ;; partly complete: hint about displaying the locked end
 	      (pg-jump-to-end-hint))))))))
 
+;;;###autoload
 (defun pg-next-error-hint ()
   "Display hint for locating error."
   (pg-hint "Use \\[proof-next-error] to go to next error location."))
 
+;;;###autoload
 (defun pg-hint (hintmsg)
   "Display a hint HINTMSG in the minibuffer, if `pg-show-hints' is non-nil.
 The function `substitute-command-keys' is called on the argument."
@@ -1076,7 +1085,7 @@ The function `substitute-command-keys' is called on the argument."
 ;; Identifier under mouse query  (added in PG 3.5)
 ;;
 
-;; FIXME: making the binding globally is perhaps a bit obnoxious, but
+;; Note: making the binding globally is perhaps a bit obnoxious, but
 ;; this modifier combination is currently unused.
 (cond
  ((not (featurep 'xemacs))
@@ -1091,8 +1100,8 @@ The function `substitute-command-keys' is called on the argument."
 	(save-selected-window
 	  (save-selected-frame
 	    (save-excursion
-	      (if (event-window event)
-		  (progn
+	      (if (featurep 'xemacs)
+		  (when (event-window event)
 		    (select-window (event-window event))
 		    (setq oldend (if (region-exists-p)
 				     (region-end)))))
@@ -1129,6 +1138,7 @@ The function `substitute-command-keys' is called on the argument."
 	(speedbar-add-supported-extension
 	 (nth 2 (assoc proof-assistant-symbol proof-assistant-table)))))
 
+;;;###autoload
 (defun proof-imenu-enable ()
   "Add or remove index menu."
   (if proof-imenu-enable
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index e72df3c6..9a68f096 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -139,10 +139,6 @@ assistant during the last group of commands.")
 If non-nil, the value counts the commands from the last command
 of the proof (starting from 1).")
 
-(defvar proof-shell-last-output nil
-  "A record of the last string seen from the proof system.
-This is raw string, for internal use only.")
-
 ;; TODO da: remove proof-terminal-string.  At the moment some
 ;; commands need to have the terminal string, some don't.
 ;; It's used variously in proof-script and proof-shell, which
@@ -154,5 +150,36 @@ This is raw string, for internal use only.")
   "End-of-line string for proof process.")
 
 
+;;
+;; Internal variables
+;; -- usually local to a couple of modules but here to avoid 
+;; compile warnings
+;;
+
+(defvar proof-shell-last-output nil
+  "A record of the last string seen from the proof system.
+This is raw string, for internal use only.")
+
+(defvar proof-assistant-settings nil
+ "A list of default values kept in Proof General for current proof assistant.
+A list of lists (SYMBOL SETTING TYPE) where SETTING is a string value
+to send to the proof assistant using the value of SYMBOL and 
+and the function `proof-assistant-format'.  The TYPE item determines
+the form of the menu entry for the setting.")
+
+(defvar pg-tracing-slow-mode nil
+  "Non-nil for slow refresh mode for tracing output.")
+
+(defvar proof-nesting-depth 0
+  "Current depth of a nested proof.
+Zero means outside a proof, 1 means inside a top-level proof, etc.
+
+This variable is maintained in `proof-done-advancing'; it is zeroed
+in `proof-shell-clear-state'.")
+
+(defvar proof-last-theorem-dependencies nil
+  "Contains the dependencies of the last theorem.  A list of strings.
+Set in `proof-shell-process-urgent-message'.")
+
 (provide 'pg-vars)
 ;; pg-vars.el ends here
diff --git a/generic/pg-xhtml.el b/generic/pg-xhtml.el
index 1070dfc0..da4eb157 100644
--- a/generic/pg-xhtml.el
+++ b/generic/pg-xhtml.el
@@ -34,7 +34,7 @@
 		    "pg"
 		    (getenv "USER")
 		    (int-to-string (emacs-pid))
-		    (char-to-string directory-sep-char)))))
+		    "/"))))
 
 (defvar pg-xhtml-file-count 0
   "Counter for generating XHTML files.")
diff --git a/generic/pg-xml.el b/generic/pg-xml.el
index 141508ff..3f9a0f37 100644
--- a/generic/pg-xml.el
+++ b/generic/pg-xml.el
@@ -9,6 +9,9 @@
 ;; XML functions for Proof General.
 ;;
 
+(eval-when-compile
+  (require 'xml-fixed))			; for compile only
+
 (require 'proof-utils) ;; for pg-internal-warning
 
 (cond
@@ -18,6 +21,10 @@
  (t					;; Otherwise use GNU Emacs distrib version.
   (require 'xml)))
 
+(defalias 'pg-xml-error 'error)
+
+
+;;
 ;; Elisp format of XML trees (see xml.el)
 ;;
 ;;    xml-list   ::= (node node ...)
@@ -44,7 +51,7 @@
     (save-excursion
       (set-buffer tempbuffer)
       (delete-region (point-min) (point-max))
-      (insert-string arg)
+      (insert arg)
       (pg-xml-parse-buffer (current-buffer) 'nomessage))))
 
 
@@ -75,7 +82,7 @@ Parsing according to `xml-parse-file' of xml.el."
     (or val
 	(if optional
 	    defaultval
-	  (pg-pgip-error "pg-xml-get-attr: Didn't find required %s attribute in %s element"
+	  (pg-xml-error "pg-xml-get-attr: Didn't find required %s attribute in %s element"
 		 attribute (xml-node-name node))))))
 
 (defun pg-xml-child-elts (node)
@@ -123,9 +130,9 @@ Parsing according to `xml-parse-file' of xml.el."
 
 (defun pg-xml-string-of (xmls)
   "Convert the XML trees in XMLS into a string (without additional indentation)."
-  (let ((insertfn    (lambda (&rest args)
-		       (setq strs (cons (reduce 'concat args) strs))))
-	strs)
+  (let* (strs
+	 (insertfn    (lambda (&rest args)
+			(setq strs (cons (reduce 'concat args) strs)))))
     (dolist (xml xmls)
       (pg-xml-output-internal xml nil insertfn))
     (reduce 'concat (reverse strs))))
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index f373b19f..a1f01c90 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -52,8 +52,26 @@ This mode is only useful with a font which can display the maths repertoire.
 
 ;;;***
 
+;;;### (autoloads (proof-associated-windows proof-associated-buffers)
+;;;;;;  "pg-assoc" "pg-assoc.el" (18318 30530))
+;;; Generated autoloads from pg-assoc.el
+
+(autoload (quote proof-associated-buffers) "pg-assoc" "\
+Return a list of the associated buffers.  
+Some may be dead/nil.
+
+\(fn)" nil nil)
+
+(autoload (quote proof-associated-windows) "pg-assoc" "\
+Return a list of the associated buffers windows.  
+Dead or nil buffers are not represented in the list.
+
+\(fn)" nil nil)
+
+;;;***
+
 ;;;### (autoloads (proof-goals-config-done) "pg-goals" "pg-goals.el"
-;;;;;;  (18317 59757))
+;;;;;;  (18317 64729))
 ;;; Generated autoloads from pg-goals.el
 
 (autoload (quote proof-goals-config-done) "pg-goals" "\
@@ -64,7 +82,7 @@ Initialise the goals buffer after the child has been configured.
 ;;;***
 
 ;;;### (autoloads (pg-pgip-askprefs pg-pgip-maybe-askpgip pg-pgip-process-packet)
-;;;;;;  "pg-pgip" "pg-pgip.el" (18316 44932))
+;;;;;;  "pg-pgip" "pg-pgip.el" (18318 22811))
 ;;; Generated autoloads from pg-pgip.el
 
 (autoload (quote pg-pgip-process-packet) "pg-pgip" "\
@@ -86,8 +104,9 @@ Send an <askprefs> message to the prover.
 ;;;***
 
 ;;;### (autoloads (pg-response-has-error-location proof-next-error
-;;;;;;  pg-response-maybe-erase proof-response-config-done proof-response-mode)
-;;;;;;  "pg-response" "pg-response.el" (18317 22894))
+;;;;;;  pg-response-display-with-face pg-response-maybe-erase proof-response-config-done
+;;;;;;  proof-response-mode) "pg-response" "pg-response.el" (18318
+;;;;;;  30542))
 ;;; Generated autoloads from pg-response.el
 
 (autoload (quote proof-response-mode) "pg-response" "\
@@ -114,6 +133,11 @@ Returns non-nil if response buffer was cleared.
 
 \(fn &optional ERASE-NEXT-TIME CLEAN-WINDOWS FORCE)" nil nil)
 
+(autoload (quote pg-response-display-with-face) "pg-response" "\
+Display STR with FACE in response buffer.
+
+\(fn STR &optional FACE)" nil nil)
+
 (autoload (quote proof-next-error) "pg-response" "\
 Jump to location of next error reported in the response buffer.
 
@@ -154,10 +178,27 @@ All of these settings are optional.
 
 ;;;***
 
-;;;### (autoloads (proof-define-assistant-command-witharg proof-define-assistant-command)
-;;;;;;  "pg-user" "pg-user.el" (18316 44932))
+;;;### (autoloads (proof-imenu-enable pg-hint pg-next-error-hint
+;;;;;;  pg-processing-complete-hint pg-jump-to-end-hint pg-response-buffers-hint
+;;;;;;  pg-slow-fontify-tracing-hint proof-electric-term-incomment-fn
+;;;;;;  proof-electric-terminator-enable proof-define-assistant-command-witharg
+;;;;;;  proof-define-assistant-command proof-interrupt-process) "pg-user"
+;;;;;;  "pg-user.el" (18318 29807))
 ;;; Generated autoloads from pg-user.el
 
+(autoload (quote proof-interrupt-process) "pg-user" "\
+Interrupt the proof assistant.  Warning! This may confuse Proof General.
+This sends an interrupt signal to the proof assistant, if Proof General
+thinks it is busy.
+
+This command is risky because when an interrupt is trapped in the
+proof assistant, we don't know whether the last command succeeded or
+not.  The assumption is that it didn't, which should be true most of
+the time, and all of the time if the proof assistant has a careful
+handling of interrupt signals.
+
+\(fn)" t nil)
+
 (autoload (quote proof-define-assistant-command) "pg-user" "\
 Define command FN to send string BODY to proof assistant, based on CMDVAR.
 BODY defaults to CMDVAR, a variable.
@@ -170,10 +211,56 @@ CMDVAR is a variable holding a function or string.  Automatically has history.
 
 \(fn FN DOC CMDVAR PROMPT &rest BODY)" nil (quote macro))
 
+(autoload (quote proof-electric-terminator-enable) "pg-user" "\
+Make sure the modeline is updated to display new value for electric terminator.
+
+\(fn)" nil nil)
+
+(autoload (quote proof-electric-term-incomment-fn) "pg-user" "\
+Used as argument to proof-assert-until-point.
+
+\(fn)" nil nil)
+
+(autoload (quote pg-slow-fontify-tracing-hint) "pg-user" "\
+Not documented
+
+\(fn)" nil nil)
+
+(autoload (quote pg-response-buffers-hint) "pg-user" "\
+Not documented
+
+\(fn &optional NEXTBUF)" nil nil)
+
+(autoload (quote pg-jump-to-end-hint) "pg-user" "\
+Not documented
+
+\(fn)" nil nil)
+
+(autoload (quote pg-processing-complete-hint) "pg-user" "\
+Display hint for showing end of locked region or processing complete.
+
+\(fn)" nil nil)
+
+(autoload (quote pg-next-error-hint) "pg-user" "\
+Display hint for locating error.
+
+\(fn)" nil nil)
+
+(autoload (quote pg-hint) "pg-user" "\
+Display a hint HINTMSG in the minibuffer, if `pg-show-hints' is non-nil.
+The function `substitute-command-keys' is called on the argument.
+
+\(fn HINTMSG)" nil nil)
+
+(autoload (quote proof-imenu-enable) "pg-user" "\
+Add or remove index menu.
+
+\(fn)" nil nil)
+
 ;;;***
 
-;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (18316
-;;;;;;  44932))
+;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (18318
+;;;;;;  28227))
 ;;; Generated autoloads from pg-xml.el
 
 (autoload (quote pg-xml-parse-string) "pg-xml" "\
@@ -184,13 +271,13 @@ Parse string in ARG, same as pg-xml-parse-buffer.
 ;;;***
 
 ;;;### (autoloads (proof-dependency-in-span-context-menu proof-depends-process-dependencies)
-;;;;;;  "proof-depends" "proof-depends.el" (18316 44932))
+;;;;;;  "proof-depends" "proof-depends.el" (18318 28443))
 ;;; Generated autoloads from proof-depends.el
 
 (autoload (quote proof-depends-process-dependencies) "proof-depends" "\
 Process dependencies reported by prover, for NAME in span GSPAN.
 Called from `proof-done-advancing' when a save is processed and
-proof-last-theorem-dependencies is set.
+`proof-last-theorem-dependencies' is set.
 
 \(fn NAME GSPAN)" nil nil)
 
@@ -202,7 +289,7 @@ Make a portion of a context-sensitive menu showing proof dependencies.
 ;;;***
 
 ;;;### (autoloads (proof-easy-config) "proof-easy-config" "proof-easy-config.el"
-;;;;;;  (18316 44932))
+;;;;;;  (18318 29272))
 ;;; Generated autoloads from proof-easy-config.el
 
 (autoload (quote proof-easy-config) "proof-easy-config" "\
@@ -215,7 +302,7 @@ the `proof-assistant-table', which see.
 ;;;***
 
 ;;;### (autoloads (proof-indent-line) "proof-indent" "proof-indent.el"
-;;;;;;  (18316 44932))
+;;;;;;  (18318 29442))
 ;;; Generated autoloads from proof-indent.el
 
 (autoload (quote proof-indent-line) "proof-indent" "\
@@ -226,7 +313,7 @@ Indent current line of proof script, if indentation enabled.
 ;;;***
 
 ;;;### (autoloads (proof-maths-menu-enable proof-maths-menu-support-available)
-;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (18316 44932))
+;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (18318 29504))
 ;;; Generated autoloads from proof-maths-menu.el
 
 (autoload (quote proof-maths-menu-support-available) "proof-maths-menu" "\
@@ -247,7 +334,7 @@ in future if we have just activated it for this buffer.
 
 ;;;### (autoloads (defpacustom proof-defpacustom-fn proof-aux-menu
 ;;;;;;  proof-menu-define-specific proof-menu-define-main proof-menu-define-keys)
-;;;;;;  "proof-menu" "proof-menu.el" (18316 44932))
+;;;;;;  "proof-menu" "proof-menu.el" (18318 26956))
 ;;; Generated autoloads from proof-menu.el
 
 (autoload (quote proof-menu-define-keys) "proof-menu" "\
@@ -290,7 +377,7 @@ evaluate can be provided instead.
 ;;;***
 
 ;;;### (autoloads (proof-mmm-enable proof-mmm-support-available)
-;;;;;;  "proof-mmm" "proof-mmm.el" (18316 44932))
+;;;;;;  "proof-mmm" "proof-mmm.el" (18318 29686))
 ;;; Generated autoloads from proof-mmm.el
 
 (autoload (quote proof-mmm-support-available) "proof-mmm" "\
@@ -309,10 +396,40 @@ in future if we have just activated it for this buffer.
 
 ;;;***
 
-;;;### (autoloads (proof-config-done proof-mode proof-insert-pbp-command)
-;;;;;;  "proof-script" "proof-script.el" (18317 59727))
+;;;### (autoloads (proof-config-done proof-mode proof-insert-pbp-command
+;;;;;;  pg-set-span-helphighlights proof-locked-region-empty-p proof-locked-region-full-p
+;;;;;;  proof-locked-end proof-unprocessed-begin) "proof-script"
+;;;;;;  "proof-script.el" (18318 30159))
 ;;; Generated autoloads from proof-script.el
 
+(autoload (quote proof-unprocessed-begin) "proof-script" "\
+Return end of locked region in current buffer or (point-min) otherwise.
+The position is actually one beyond the last locked character.
+
+\(fn)" nil nil)
+
+(autoload (quote proof-locked-end) "proof-script" "\
+Return end of the locked region of the current buffer.
+Only call this from a scripting buffer.
+
+\(fn)" nil nil)
+
+(autoload (quote proof-locked-region-full-p) "proof-script" "\
+Non-nil if the locked region covers all the buffer's non-whitespace.
+Works on any buffer.
+
+\(fn)" nil nil)
+
+(autoload (quote proof-locked-region-empty-p) "proof-script" "\
+Non-nil if the locked region is empty.  Works on any buffer.
+
+\(fn)" nil nil)
+
+(autoload (quote pg-set-span-helphighlights) "proof-script" "\
+Set the help echo message, default highlight, and keymap for SPAN.
+
+\(fn SPAN &optional NOHIGHLIGHT)" nil nil)
+
 (autoload (quote proof-insert-pbp-command) "proof-script" "\
 Insert CMD into the proof queue.
 
@@ -337,7 +454,7 @@ finish setup which depends on specific proof assistant configuration.
 ;;;;;;  proof-shell-invisible-cmd-get-result proof-shell-invisible-command
 ;;;;;;  proof-shell-wait proof-extend-queue proof-start-queue proof-shell-insert
 ;;;;;;  proof-shell-available-p proof-shell-live-buffer proof-shell-ready-prover)
-;;;;;;  "proof-shell" "proof-shell.el" (18317 59753))
+;;;;;;  "proof-shell" "proof-shell.el" (18318 29860))
 ;;; Generated autoloads from proof-shell.el
 
 (autoload (quote proof-shell-ready-prover) "proof-shell" "\
@@ -448,7 +565,7 @@ processing.
 ;;;***
 
 ;;;### (autoloads (proof-splash-message proof-splash-display-screen)
-;;;;;;  "proof-splash" "proof-splash.el" (18316 44931))
+;;;;;;  "proof-splash" "proof-splash.el" (18318 30049))
 ;;; Generated autoloads from proof-splash.el
 
 (autoload (quote proof-splash-display-screen) "proof-splash" "\
@@ -466,8 +583,8 @@ Make sure the user gets welcomed one way or another.
 
 ;;;***
 
-;;;### (autoloads (proof-format) "proof-syntax" "proof-syntax.el"
-;;;;;;  (18316 44931))
+;;;### (autoloads (proof-splice-separator proof-format) "proof-syntax"
+;;;;;;  "proof-syntax.el" (18318 27344))
 ;;; Generated autoloads from proof-syntax.el
 
 (autoload (quote proof-format) "proof-syntax" "\
@@ -477,10 +594,15 @@ may be a string or sexp evaluated to get a string.
 
 \(fn ALIST STRING)" nil nil)
 
+(autoload (quote proof-splice-separator) "proof-syntax" "\
+Splice SEP into list of STRINGS.
+
+\(fn SEP STRINGS)" nil nil)
+
 ;;;***
 
 ;;;### (autoloads (proof-toolbar-scripting-menu proof-toolbar-setup)
-;;;;;;  "proof-toolbar" "proof-toolbar.el" (18316 44931))
+;;;;;;  "proof-toolbar" "proof-toolbar.el" (18318 30407))
 ;;; Generated autoloads from proof-toolbar.el
 
 (autoload (quote proof-toolbar-setup) "proof-toolbar" "\
@@ -500,7 +622,7 @@ Menu made from the Proof General toolbar commands.
 
 ;;;### (autoloads (proof-x-symbol-config-output-buffer proof-x-symbol-shell-config
 ;;;;;;  proof-x-symbol-decode-region proof-x-symbol-enable proof-x-symbol-support-maybe-available)
-;;;;;;  "proof-x-symbol" "proof-x-symbol.el" (18317 59366))
+;;;;;;  "proof-x-symbol" "proof-x-symbol.el" (18317 64729))
 ;;; Generated autoloads from proof-x-symbol.el
 
 (autoload (quote proof-x-symbol-support-maybe-available) "proof-x-symbol" "\
@@ -538,12 +660,12 @@ Configure the current output buffer (goals/response/trace) for X-Symbol.
 ;;;### (autoloads nil nil ("../lib/holes-load.el" "../lib/local-vars-list.el"
 ;;;;;;  "../lib/pg-dev.el" "../lib/proof-compat.el" "../lib/span-extent.el"
 ;;;;;;  "../lib/span-overlay.el" "../lib/span.el" "../lib/unichars.el"
-;;;;;;  "../lib/xml-fixed.el" "../lib/xmlunicode.el" "pg-assoc.el"
-;;;;;;  "pg-autotest.el" "pg-custom.el" "pg-metadata.el" "pg-pbrpm.el"
-;;;;;;  "pg-pgip-old.el" "pg-vars.el" "pg-xhtml.el" "proof-config.el"
-;;;;;;  "proof-site.el" "proof-utils.el" "proof.el" "test-compile.el"
-;;;;;;  "test-mac.el" "test-mac2.el" "test-req.el" "test-req2.el")
-;;;;;;  (18317 59766 407486))
+;;;;;;  "../lib/xml-fixed.el" "../lib/xmlunicode.el" "pg-autotest.el"
+;;;;;;  "pg-custom.el" "pg-metadata.el" "pg-pbrpm.el" "pg-pgip-old.el"
+;;;;;;  "pg-vars.el" "pg-xhtml.el" "proof-config.el" "proof-site.el"
+;;;;;;  "proof-utils.el" "proof.el" "test-compile.el" "test-mac.el"
+;;;;;;  "test-mac2.el" "test-req.el" "test-req2.el") (18318 30548
+;;;;;;  438094))
 
 ;;;***
 
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index 0f1c4eff..7605515f 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -12,7 +12,11 @@
 ;; within proofs.  Code rewritten by David Aspinall.
 ;; 
 
+(require 'cl)
 (require 'span)
+(require 'pg-vars)
+(require 'proof-config)
+(require 'proof-autoloads)
 
 ;; Variables
 
@@ -71,7 +75,7 @@ This is done using `proof-depends-module-name-for-buffer' and
 (defun proof-depends-process-dependencies (name gspan)
   "Process dependencies reported by prover, for NAME in span GSPAN.
 Called from `proof-done-advancing' when a save is processed and
-proof-last-theorem-dependencies is set."
+`proof-last-theorem-dependencies' is set."
 
   (span-set-property gspan 'dependencies
 		     ;; Ancestors of NAME are in the second component.
diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el
index c93cb641..0752003b 100644
--- a/generic/proof-easy-config.el
+++ b/generic/proof-easy-config.el
@@ -6,11 +6,13 @@
 ;;
 ;; $Id$
 ;;
-;; Future version might copy settings instead; consider how best to
+;; Future versions might copy settings instead; consider how best to
 ;; interface with customization mechanism so a new prover can be
 ;; configured by editing inside custom buffers.
 ;;
 
+(require 'proof-site)			; proof-assistant, proof-assistant-symbol
+
 (defconst proof-easy-config-derived-modes-table
   '((""         "script"     proof-mode (proof-config-done))
     ("shell"    "shell"      proof-shell-mode (proof-shell-config-done))
@@ -58,11 +60,11 @@
     ;; in the macro matches that in `proof-assistant-table'
     ;; and have the right type.
     (unless (symbolp sym)
-      (error "proof-easy-config: first argument (%s) should be a symbol"
+      (error "Macro proof-easy-config: first argument (%s) should be a symbol"
 	     sym))
     (unless (stringp name)
-      (error "proof-easy-config: second argument (%s) should be a string"
-	     string))
+      (error "Macro proof-easy-config: second argument (%s) should be a string"
+	     name))
     (cond
      ((or 
        (and (boundp 'proof-assistant) proof-assistant 
diff --git a/generic/proof-indent.el b/generic/proof-indent.el
index df5014cf..ab0a522c 100644
--- a/generic/proof-indent.el
+++ b/generic/proof-indent.el
@@ -6,6 +6,11 @@
 ;; $Id$
 ;;
 
+(require 'proof-config)			; config variables
+(require 'proof-utils)			; proof-ass
+(require 'proof-syntax)			; p-looking-at-safe, p-re-search
+(require 'proof-autoloads)		; p-locked-end
+
 (defun proof-indent-indent ()
   "Determine indentation caused by syntax element at current point."
   (cond
diff --git a/generic/proof-maths-menu.el b/generic/proof-maths-menu.el
index 726668cc..7f488fa1 100644
--- a/generic/proof-maths-menu.el
+++ b/generic/proof-maths-menu.el
@@ -19,6 +19,7 @@
 ;;
 
 (eval-when-compile
+  (require 'maths-menu)	  ; dynamically loaded at runtime
   (require 'proof-utils)) ; proof-ass, proof-eval-when-ready-for-assistant
 
 
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index b562d31a..75068e41 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -7,9 +7,11 @@
 ;; $Id$
 ;;
 
-(require 'pg-user)         ; user commands used here
-(require 'proof-utils)     ; proof-deftoggle, proof-eval-when-ready-for-assistant
-(require 'proof-autoloads) ; 
+(eval-when-compile
+  (defvar proof-mode-map nil)
+  (defvar proof-assistant-menu nil))	; avoid compile warnings
+
+(require 'proof)           ; proof-deftoggle, proof-eval-when-ready-for-assistant
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
@@ -149,6 +151,9 @@ without adjusting window layout."
 
 ;; The proof assistant specific menu
 
+(defvar proof-menu-favourites nil
+  "The Proof General favourites menu for the current proof assistant.")
+
 ;;;###autoload
 (defun proof-menu-define-specific ()
   (easy-menu-define 
@@ -527,9 +532,6 @@ without adjusting window layout."
 ;;; Favourites mechanism for prover-specific menu
 ;;;
 
-(defvar proof-menu-favourites nil
-  "The Proof General favourites menu for the current proof assistant.")
-
 (defun proof-menu-define-favourites-menu ()
   "Return menu generated from `PA-favourites'."
   (let ((favs (reverse (proof-ass favourites))) ents)
@@ -653,13 +655,6 @@ KEY is the optional key binding."
 ;;; Proof assistant settings mechanism.
 ;;;
 
-(defvar proof-assistant-settings nil
- "A list of default values kept in Proof General for current proof assistant.
-A list of lists (SYMBOL SETTING TYPE) where SETTING is a string value
-to send to the proof assistant using the value of SYMBOL and 
-and the function `proof-assistant-format'.  The TYPE item determines
-the form of the menu entry for the setting.")
-
 (defvar proof-menu-settings nil
   "Settings submenu for Proof General.")
 
@@ -875,6 +870,23 @@ NB: if no settings are configured, this has no effect."
 	(apply 'concat (mapcar evalifneeded 
 			       proof-assistant-settings)))))
 
+(defvar proof-assistant-format-table 
+  (list
+   (cons "%b" '(proof-assistant-format-bool curvalue))
+   (cons "%i" '(proof-assistant-format-int curvalue))
+   (cons "%s" '(proof-assistant-format-string curvalue)))
+  "Table to use with `proof-format' for formatting CURVALUE for assistant.
+NB: variable curvalue is dynamically scoped (used in proof-assistant-format).")
+
+(defun proof-assistant-format-bool (value)
+  (if value proof-assistant-true-value proof-assistant-false-value))
+
+(defun proof-assistant-format-int (value)
+  (funcall proof-assistant-format-int-fn value))
+
+(defun proof-assistant-format-string (value)
+  (funcall proof-assistant-format-string-fn value))
+
 (defun proof-assistant-format (string curvalue)
   "Replace a format characters %b %i %s in STRING by formatted CURVALUE.
 Formatting suitable for current proof assistant, controlled by
@@ -899,22 +911,6 @@ value) and the second for false."
 	(funcall proof-assistant-setting-format setting)
       setting)))
 
-(defvar proof-assistant-format-table 
-  (list
-   (cons "%b" '(proof-assistant-format-bool curvalue))
-   (cons "%i" '(proof-assistant-format-int curvalue))
-   (cons "%s" '(proof-assistant-format-string curvalue)))
-  "Table to use with `proof-format' for formatting CURVALUE for assistant.
-NB: variable curvalue is dynamically scoped (used in proof-assistant-format).")
-
-(defun proof-assistant-format-bool (value)
-  (if value proof-assistant-true-value proof-assistant-false-value))
-
-(defun proof-assistant-format-int (value)
-  (funcall proof-assistant-format-int-fn value))
-
-(defun proof-assistant-format-string (value)
-  (funcall proof-assistant-format-string-fn value))
 
 
 
diff --git a/generic/proof-mmm.el b/generic/proof-mmm.el
index e2d9559d..5bb22f0c 100644
--- a/generic/proof-mmm.el
+++ b/generic/proof-mmm.el
@@ -22,6 +22,7 @@
 ;; It should define an MMM submode class called <foo>.
 
 (eval-when-compile
+  (require 'mmm-auto)	  ; loaded dynamically at runtime
   (require 'proof-utils)) ; for proof-ass, proof-eval-when-ready-for-assistant
 
 (require 'proof-site)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 7b70a64f..129e65b7 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -11,14 +11,10 @@
 
 ;;; Code:
 
-(eval-when-compile 
-  (require 'proof-utils))		; for macros
-
 (require 'cl)				; various
-(require 'proof)			; loader
-(require 'proof-syntax)		        ; utils for manipulating syntax
 (require 'span)				; abstraction of overlays/extents
-(require 'pg-user)			; user-level commands
+(require 'proof)			; loader (& proof-utils macros)
+(require 'proof-syntax)		        ; utils for manipulating syntax
 (require 'proof-menu)			; menus for script mode
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -30,17 +26,6 @@
 
 ;; Scripting variables
 
-(defvar proof-last-theorem-dependencies nil
-  "Contains the dependencies of the last theorem.  A list of strings.
-Set in `proof-shell-process-urgent-message'.")
-
-(defvar proof-nesting-depth 0
-  "Current depth of a nested proof.
-Zero means outside a proof, 1 means inside a top-level proof, etc.
-
-This variable is maintained in proof-done-advancing; it is zeroed
-in proof-shell-clear-state.")
-
 (defvar proof-element-counters nil
   "Table of (name .  count) pairs, counting elements in scripting buffer.")
 
@@ -349,6 +334,7 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}."
 ;; Buffer position functions
 ;;
 
+;;;###autoload
 (defun proof-unprocessed-begin ()
   "Return end of locked region in current buffer or (point-min) otherwise.
 The position is actually one beyond the last locked character."
@@ -380,6 +366,7 @@ when a queue of commands is being processed."
 ;; FIXME: get rid of/rework this function.  Some places expect this to
 ;; return nil if locked region is empty. Moreover, it confusingly
 ;; returns the point past the end of the locked region.
+;;;###autoload
 (defun proof-locked-end ()
   "Return end of the locked region of the current buffer.
 Only call this from a scripting buffer."
@@ -396,6 +383,7 @@ Only call this from a scripting buffer."
 ;; (as processed files) too.
 ;;
 
+;;;###autoload
 (defun proof-locked-region-full-p ()
   "Non-nil if the locked region covers all the buffer's non-whitespace.
 Works on any buffer."
@@ -404,6 +392,7 @@ Works on any buffer."
     (skip-chars-backward " \t\n")
     (>= (proof-unprocessed-begin) (point))))
 
+;;;###autoload
 (defun proof-locked-region-empty-p ()
   "Non-nil if the locked region is empty.  Works on any buffer."
   (eq (proof-unprocessed-begin) (point-min)))
@@ -681,6 +670,19 @@ NAME does not need to be unique."
      ((eq type 'proverproc)
 		           "Prover-processed"))))
 
+(defvar pg-span-context-menu-keymap
+    (let ((map (make-sparse-keymap
+		"Keymap for context-sensitive menus on spans")))
+      (cond
+       ((featurep 'xemacs)
+	(define-key map [button3] 'pg-span-context-menu))
+       ((not (featurep 'xemacs))
+	(define-key map [down-mouse-3] 'pg-span-context-menu)))
+      map)
+    "Keymap for the span context menu.")
+
+
+;;;###autoload
 (defun pg-set-span-helphighlights (span &optional nohighlight)
   "Set the help echo message, default highlight, and keymap for SPAN."
   (let ((helpmsg (concat (pg-span-name span) ""))) ;;   " region"
@@ -694,7 +696,10 @@ NAME does not need to be unique."
 	   " ("
 	   (if (span-property span 'idiom)
 	       "with point in region, \\[pg-toggle-visibility] to show/hide; ")
-	   "\\[popup-mode-menu] for menu)"))))
+	   (if (featurep 'xemacs)
+	       "\\[popup-mode-menu]"
+	     "\\<pg-span-context-menu-keymap>\\[pg-span-context-menu]")
+	     " for menu)"))))
     (span-set-property span 'keymap pg-span-context-menu-keymap)
     (unless nohighlight
       (span-set-property span 'mouse-face 'proof-mouse-highlight-face))))
@@ -1896,6 +1901,7 @@ This version is used when `proof-script-command-end-regexp' is set."
   (save-excursion
     (let*
 	((commentre   (concat "[ \t\n]*" proof-script-comment-start-regexp))
+	 prev alist			; used below
 	 (add-segment-for-cmd		; local function: advances "prev"
 	  (lambda ()
 	    (let ((cmdend (point)) start)
@@ -1929,7 +1935,7 @@ This version is used when `proof-script-command-end-regexp' is set."
 				      cmdend) alist))
 	      (setq prev cmdend)
 	      (goto-char cmdend))))
-	 alist prev cmdfnd startpos tmp)
+	  cmdfnd startpos tmp)
       (goto-char (proof-queue-or-locked-end))
       (setq prev (point))
       (skip-chars-forward " \t\n")
@@ -2761,10 +2767,7 @@ finish setup which depends on specific proof assistant configuration."
 	  (vconcat [(control c)] (vector proof-terminal-char))
 	  'proof-electric-terminator-toggle)
 	(define-key proof-mode-map (vector proof-terminal-char)
-	  'proof-electric-terminator)))
-  ;; It's ugly, but every script buffer has a local copy changed in
-  ;; sync by the fn proof-electric-terminator-enable
-  (setq proof-electric-terminator proof-electric-terminator-enable)
+	  'proof-electric-terminator-toggle)))
 
   (make-local-variable 'indent-line-function)
   (setq indent-line-function 'proof-indent-line)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index a30711d9..f8724c9d 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1649,9 +1649,6 @@ by the filter is to send the next command from the queue."
 (defvar pg-last-tracing-output-time nil
   "Time of last tracing output, as recorded by (current-time).")
 
-(defvar pg-tracing-slow-mode nil
-  "Non-nil for slow refresh mode for tracing output.")
-
 (defconst pg-slow-mode-duration 2
   "Maximum duration of slow mode in seconds.")
 
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index d4fe8695..05208a63 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -8,8 +8,11 @@
 ;;
 ;;
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Customization of splash screen (was in proof-config)
+(require 'proof-site)
+
+;;
+;; Customization of splash screen 
+;;
 
 (defcustom proof-splash-enable t
   "*If non-nil, display a splash screen when Proof General is loaded."
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 5a96ec05..87831f50 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -9,8 +9,10 @@
 ;;
 
 (require 'font-lock)
+(require 'proof-config)			; proof-case-fold-search
+(require 'proof-compat)			; proof-buffer-syntactic-context
 
-;; FIXME da: would regexp-opt be better here?  Or maybe
+;; TODO da: would regexp-opt be better here?  Or maybe
 ;;  (concat "\\<" (regexp-opt l) "\\>")
 (defun proof-ids-to-regexp (l)
   "Maps a non-empty list of tokens `l' to a regexp matching any element"
@@ -280,6 +282,7 @@ Any other %-prefixed character inserts itself."
     (if acc (insert acc))
     (if pos (goto-char pos))))
 
+;;;###autoload
 (defun proof-splice-separator (sep strings)
   "Splice SEP into list of STRINGS."
   (let (stringsep)
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index b00ffa72..aca064fe 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -30,6 +30,11 @@
 
 (eval-when-compile
   (require 'proof-utils))
+
+(require 'span)
+(require 'proof-config)
+(require 'proof-autoloads)
+
 ;;
 ;; Function, icon, button names
 ;; 
@@ -236,8 +241,8 @@ to the default toolbar."
 
 (defun proof-toolbar-setup-refresh ()
   "Enable the XEmacs hackery to update the toolbar."
-  (if  proof-toolbar-use-button-enablers
-      (progn
+  (if (featurep 'xemacs) ; skip compilation on GNU Emacs
+      (when  proof-toolbar-use-button-enablers 
 	;; Set the callback for updating the enablers
 	(add-hook 'proof-state-change-hook 'proof-toolbar-refresh)
 	;; Also call it whenever text changes in this buffer,
@@ -257,10 +262,11 @@ to the default toolbar."
 
 (defun proof-toolbar-disable-refresh ()
   "Disable the XEmacs hackery to update the toolbar."
-  (remove-hook 'proof-state-change-hook 'proof-toolbar-refresh)
-  (remove-hook 'after-change-functions 'proof-toolbar-refresh)
-  (if proof-toolbar-itimer (delete-itimer proof-toolbar-itimer))
-  (setq proof-toolbar-itimer nil))
+  (when (featurep 'xemacs) ; skip compilation on GNU Emacs
+    (remove-hook 'proof-state-change-hook 'proof-toolbar-refresh)
+    (remove-hook 'after-change-functions 'proof-toolbar-refresh)
+    (if proof-toolbar-itimer (delete-itimer proof-toolbar-itimer))
+    (setq proof-toolbar-itimer nil)))
 
 (deflocal proof-toolbar-refresh-flag nil
   "Flag indicating that the toolbar should be refreshed.")
@@ -286,24 +292,26 @@ to the default toolbar."
   "Force refresh of toolbar display to re-evaluate enablers.
 This function needs to be called anytime that enablers may have 
 changed state."
-  (if ;; Be careful to only add to correct buffer, and if it's live
-       (buffer-live-p buf)
-      (let ((enabler-state (mapcar 'eval proof-toolbar-enablers)))
-	(if 
-	    (not (equal enabler-state proof-toolbar-enablers-last-state))
-	    (progn
-	      (setq proof-toolbar-enablers-last-state enabler-state)
-	      ;; The official way to do this should be 
-	      ;; (set-specifier-dirty-flag default-toolbar)
-	      ;; but it doesn't work, so we do what VM does instead,
-	      ;; removing and re-adding.  
-	      (remove-specifier default-toolbar buf)
-	      (set-specifier default-toolbar proof-toolbar buf)
-	      ;; We set the dirty flag as well just in case it helps...
-	      (set-specifier-dirty-flag default-toolbar)
-	      (setq proof-toolbar-refresh-flag nil))))
-    ;; Kill off this itimer if it's owning buffer has died
-    (delete-itimer current-itimer)))
+  (if (featurep 'xemacs)		; skip compilation on GNU Emacs
+      (if ;; Be careful to only add to correct buffer, and if it's live
+	  (buffer-live-p buf)
+	  (let ((enabler-state (mapcar 'eval proof-toolbar-enablers)))
+	    (if 
+		(not (equal enabler-state proof-toolbar-enablers-last-state))
+		(progn
+		  (setq proof-toolbar-enablers-last-state enabler-state)
+		  (when (featurep 'xemacs)
+		    ;; The official way to do this should be 
+		    ;; (set-specifier-dirty-flag default-toolbar)
+		    ;; but it doesn't work, so we do what VM does instead,
+		    ;; removing and re-adding.  
+		    (remove-specifier default-toolbar buf)
+		    (set-specifier default-toolbar proof-toolbar buf)
+		    ;; We set the dirty flag as well just in case it helps...
+		    (set-specifier-dirty-flag default-toolbar))
+		  (setq proof-toolbar-refresh-flag nil))))
+	;; Kill off this itimer if it's owning buffer has died
+	(delete-itimer current-itimer))))
 
 ;;
 ;; =================================================================
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index dbe4188b..49d32813 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -18,6 +18,11 @@
 
 (require 'proof-site)			; basic vars
 (require 'proof-compat)		        ; for pg-defface-window-systems
+(require 'proof-config)			; config vars
+(require 'bufhist)			; bufhist 
+(require 'proof-syntax)			; syntax utils
+(require 'proof-autoloads)		; interface fns
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;