Clean compile

15 files changed, 310 insertions, 227 deletions

diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index 5fb14f0b..994247cf 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -16,6 +16,7 @@
 ;; $Id$
 
 (require 'proof)
+(require 'proof-shell)
 
 ;;; Commentary:
 ;;
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index f98859ba..b45a0f71 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -14,12 +14,11 @@
 (eval-when-compile
   (require 'easymenu)			; easy-menu-add, etc
   (require 'cl)				; incf
-  (require 'span))			; span-*
+  (require 'span)			; span-*
+  (defvar proof-goals-mode-menu)	; defined by macro below
+  (defvar proof-assistant-menu))	; defined by macro in proof-menu
 
-(require 'proof-utils)
 (require 'pg-assoc)
-(require 'bufhist)
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index 2e8a75b0..76fb230d 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -19,9 +19,11 @@
 ;;
 
 ;;; Code:
-(require 'proof)
 (require 'span)
-(require 'proof-script)
+(eval-when-compile
+  (require 'proof-utils))
+
+(require 'proof)
 
 ;;;
 ;;; Configuration
@@ -101,8 +103,10 @@ Matches the region to be returned.")
 ;	(phox-mode)
 ; da: proof-mode-for-script should do it
 ; cr: proof-mode-for-script is not defined in 3.7
-	(if (functionp 'proof-mode-for-script)
-	    (funcall 'proof-mode-for-shell) (funcall 'proof-mode))
+;	(if (functionp 'proof-mode-for-script)
+;	    (funcall 'proof-mode-for-shell) (funcall 'proof-mode))
+; da: it's the name of a function, not fn itself. See pg-vars
+	(funcall proof-mode-for-script)
 	(add-hook 'after-change-functions 'pg-pbrpm-menu-change-hook nil t)
     (pg-pbrpm-erase-buffer-menu)))
   (set-buffer pg-pbrpm-buffer-menu))
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index a32500fe..94400d1a 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -1,6 +1,6 @@
 ;; pg-pgip.el --- PGIP manipulation for Proof General
 ;;
-;; Copyright (C) 2000-2002 LFCS Edinburgh.
+;; Copyright (C) 2000-2002, 2009 LFCS Edinburgh.
 ;; Author:   David Aspinall <David.Aspinall@ed.ac.uk>
 ;; License:  GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -29,7 +29,11 @@
 
 (require 'cl)				; incf
 (require 'pg-xml)			;
-(require 'proof-config)			;; config variables
+
+(declare-function pg-response-warning "pg-response")
+(declare-function pg-response-message "pg-response")
+(declare-function proof-segment-up-to "proof-script") 
+
 
 ;;; Code:
 (defalias 'pg-pgip-debug   'proof-debug)
@@ -269,8 +273,8 @@ Return a symbol representing the PGIP command processed, or nil."
 	(text     (pg-pgip-get-displaytext node)))
     ;; TODO: display and cache the value in a dedicated buffer
     ;; FIXME: should idvalue have a context?
-    (proof-message text)))
-
+    (pg-response-message text)))
+    
 ;;
 ;; Menu configuration [TODO]
 ;;
@@ -310,11 +314,11 @@ Return a symbol representing the PGIP command processed, or nil."
 
 (defun pg-pgip-process-normalresponse (node)
   (let ((text     (pg-pgip-get-displaytext node)))
-    (proof-message text)))
+    (pg-response-message text)))
 
 (defun pg-pgip-process-errorresponse (node)
   (let ((text     (pg-pgip-get-displaytext node)))
-    (proof-warning text)))
+    (pg-response-warning text)))
 
 (defun pg-pgip-process-scriptinsert (node)
   (let ((text     (pg-pgip-get-displaytext node)))
diff --git a/generic/pg-response.el b/generic/pg-response.el
index e5edf640..b5196014 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -17,9 +17,10 @@
 
 (eval-when-compile
   (require 'easymenu)	  ; easy-menu-add
-  (require 'proof-utils)) ; deflocal, proof-eval-when-ready-for-assistant
+  (require 'proof-utils)  ; deflocal, proof-eval-when-ready-for-assistant
+  (defvar proof-response-mode-menu nil)
+  (defvar proof-assistant-menu nil))
 
-(require 'bufhist)
 (require 'pg-assoc)
 
 
@@ -312,6 +313,20 @@ is set to nil, so responses are not cleared automatically."
 	(bufhist-checkpoint-and-erase))
     (set-buffer-modified-p nil)))
 
+;;;###autoload
+(defun pg-response-message (&rest args)
+  "Issue the message ARGS in the response buffer and display it."
+  (pg-response-display-with-face (apply 'concat args))
+  (proof-display-and-keep-buffer proof-response-buffer))
+
+;;;####autoload
+(defun pg-response-warning (&rest args)
+  "Issue the warning ARGS in the response buffer and display it.
+The warning is coloured with proof-warning-face."
+  (pg-response-display-with-face (apply 'concat args) 'proof-warning-face)
+  (proof-display-and-keep-buffer proof-response-buffer))
+
+
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -394,7 +409,8 @@ and start at the first error."
 		  ;; Find the error location in the error buffer
 		  (set-buffer errbuf)
 		  ;; FIXME: no handling of selective display here
-		  (goto-line line)
+		  (with-no-warnings ; "interactive only"
+		   (goto-line line))
 		  (if (and column (> column 1))
 		      (move-to-column (1- column)))))
 	    (setq pg-response-next-error nil)
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 2dc04816..52908b72 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -18,12 +18,14 @@
 (require 'span)
 (require 'scomint)
 
-(require 'proof)			; loader
-(require 'proof-script)			; we build on proof-script
+(require 'proof-script)	        ; we build on proof-script
 
 (eval-when-compile
+  (require 'cl)
   (require 'completion))		; loaded dynamically at runtime
 
+; defined in proof-script/proof-setup-parsing-mechanism
+(declare-function proof-segment-up-to "proof-script") 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -42,6 +44,7 @@ Assumes that point is at the end of a command."
 ;; forward for a "new" command may insert spaces or new lines.  Moving
 ;; forward for the "next" command does not.
 
+;;;###autoload
 (defun proof-script-new-command-advance ()
   "Move point to a nice position for a new command.
 Assumes that point is at the end of a command."
@@ -104,11 +107,60 @@ Assumes script buffer is current."
 	       (> dest (point)))
 	  (goto-char dest))))))
 
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Further movement commands 
+;;
+
+;; TODO da: the next function is messy.
+(defun proof-goto-command-start ()
+  "Move point to start of current (or final) command of the script."
+  (interactive)
+  (let* ((cmd (span-at (point) 'type))
+	 (start (if cmd (span-start cmd))))
+    (if start
+	(progn
+	  ;; BUG: only works for unclosed proofs.
+	  (goto-char start))
+      (let ((semis (nth 1 (proof-segment-up-to (point) t))))
+	(if (eq 'unclosed-comment (car-safe semis))
+	    (setq semis (cdr-safe semis)))
+	(if (nth 2 semis) ; fetch end point of previous command
+	      (goto-char (nth 2 semis))
+	  ;; no previous command: just next to end of locked
+	  (goto-char (proof-locked-end)))))
+    ;; Oddities of this function: if we're beyond the last proof
+    ;; command, it jumps back to the last command.  Could alter this
+    ;; by spotting that command end of last of semis is before
+    ;; point.  Also, behaviour with comments is different depending
+    ;; on whether locked or not.
+    (skip-chars-forward " \t\n")))
+
+(defun proof-goto-command-end ()
+  "Set point to end of command at point."
+  (interactive)
+  (let ((cmd (span-at (point) 'type)))
+    (if cmd
+	(goto-char (span-end cmd))
+      (let ((semis (save-excursion
+		     (proof-segment-up-to-using-cache (point)))))
+	(if semis
+	    (progn
+	      (goto-char (nth 2 (car semis)))
+	      (skip-chars-backward " \t\n")
+	      (unless (eq (point) (point-min))
+		(backward-char))))))))
+
+
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Processing commands
 ;;
 
+;;;###autoload
 (defun proof-goto-point ()
   "Assert or retract to the command at current position.
 Calls `proof-assert-until-point' or `proof-retract-until-point' as
@@ -215,49 +267,6 @@ the proof script."
 	 (error "Not proving")))
      (if span (proof-maybe-follow-locked-end (span-start span)))))
 
-;;
-;; Movement commands
-;;
-
-;; TODO da: the next function is messy.
-(defun proof-goto-command-start ()
-  "Move point to start of current (or final) command of the script."
-  (interactive)
-  (let* ((cmd (span-at (point) 'type))
-	 (start (if cmd (span-start cmd))))
-    (if start
-	(progn
-	  ;; BUG: only works for unclosed proofs.
-	  (goto-char start))
-      (let ((semis (nth 1 (proof-segment-up-to (point) t))))
-	(if (eq 'unclosed-comment (car-safe semis))
-	    (setq semis (cdr-safe semis)))
-	(if (nth 2 semis) ; fetch end point of previous command
-	      (goto-char (nth 2 semis))
-	  ;; no previous command: just next to end of locked
-	  (goto-char (proof-locked-end)))))
-    ;; Oddities of this function: if we're beyond the last proof
-    ;; command, it jumps back to the last command.  Could alter this
-    ;; by spotting that command end of last of semis is before
-    ;; point.  Also, behaviour with comments is different depending
-    ;; on whether locked or not.
-    (skip-chars-forward " \t\n")))
-
-(defun proof-goto-command-end ()
-  "Set point to end of command at point."
-  (interactive)
-  (let ((cmd (span-at (point) 'type)))
-    (if cmd
-	(goto-char (span-end cmd))
-      (let ((semis (save-excursion
-		     (proof-segment-up-to-using-cache (point)))))
-	(if semis
-	    (progn
-	      (goto-char (nth 2 (car semis)))
-	      (skip-chars-backward " \t\n")
-	      (unless (eq (point) (point-min))
-		(backward-char))))))))
-
 
 ;;
 ;; Mouse functions
@@ -613,8 +622,9 @@ last use time, to discourage saving these into the users database."
 ;; NB: completion table is expected to be set when proof-script
 ;; is loaded!  Can call proof-script-add-completions if the table
 ;; is updated.
-(eval-after-load "completion"
-  '(proof-add-completions))
+(unless noninteractive ; during compilation
+  (eval-after-load "completion"
+  '(proof-add-completions)))
 
 (defun proof-script-complete (&optional arg)
   "Like `complete' but case-fold-search set to proof-case-fold-search."
@@ -623,20 +633,6 @@ last use time, to discourage saving these into the users database."
     (complete arg)))
 
 
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Function to insert last prover output in comment.
-;; Requested/suggested by Christophe Raffalli
-;;
-
-(defun pg-insert-last-output-as-comment ()
-  "Insert the last output from the proof system as a comment in the proof script."
-  (interactive)
-  (if proof-shell-last-output
-      (let  ((beg (point)))
-	(insert (proof-shell-strip-output-markup proof-shell-last-output))
-	(comment-region beg (point)))))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index e402fb98..cf4e855b 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -162,14 +162,42 @@ of the proof (starting from 1).")
 
 ;;
 ;; Internal variables
-;; -- usually local to a couple of modules but here to avoid
-;; compile warnings
+;; -- usually local to a couple of modules and perhaps inspected
+;;    by prover modes
+;; -- here to avoid compiler warnings and minimise requires.
 ;;
 
+(defvar proof-shell-silent nil
+  "A flag, non-nil if PG thinks the prover is silent.")
+
+(defvar proof-shell-last-prompt ""
+  "A raw record of the last prompt seen from the proof system.
+This is the string matched by `proof-shell-annotated-prompt-regexp'.")
+
 (defvar proof-shell-last-output ""
   "A record of the last string seen from the proof system.
 This is raw string, for internal use only.")
 
+(defvar proof-shell-last-output-kind nil
+  "A symbol denoting the type of the last output string from the proof system.
+Specifically:
+
+ 'interrupt	 An interrupt message
+ 'error		 An error message
+ 'loopback	 A command sent from the PA to be inserted into the script
+ 'response	 A response message
+ 'goals		 A goals (proof state) display
+ 'systemspecific Something specific to a particular system,
+		  -- see `proof-shell-handle-output-system-specific'
+
+The output corresponding to this will be in `proof-shell-last-output'.
+
+See also `proof-shell-proof-completed' for further information about
+the proof process output, when ends of proofs are spotted.
+
+This variable can be used for instance specific functions which want
+to examine `proof-shell-last-output'.")
+
 (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 DESCR) where SETTING is a string value
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 703258ff..798fb440 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -8,7 +8,7 @@
 ;;;***
 
 ;;;### (autoloads (bufhist-exit bufhist-init bufhist-mode) "bufhist"
-;;;;;;  "../lib/bufhist.el" (19108 53141))
+;;;;;;  "../lib/bufhist.el" (19110 10300))
 ;;; Generated autoloads from ../lib/bufhist.el
 
 (autoload 'bufhist-mode "bufhist" "\
@@ -41,15 +41,15 @@ Stop keeping ring history for current buffer.
 
 ;;;### (autoloads (holes-insert-and-expand holes-abbrev-complete
 ;;;;;;  holes-mode holes-set-make-active-hole) "holes" "../lib/holes.el"
-;;;;;;  (19107 61958))
+;;;;;;  (19110 10300))
 ;;; Generated autoloads from ../lib/holes.el
 
-(autoload (quote holes-set-make-active-hole) "holes" "\
+(autoload 'holes-set-make-active-hole "holes" "\
 Make a new hole between START and END or at point, and make it active.
 
 \(fn &optional START END)" t nil)
 
-(autoload (quote holes-mode) "holes" "\
+(autoload 'holes-mode "holes" "\
 Toggle Holes minor mode.
 With arg, turn Outline minor mode on if arg is positive, off otherwise.
 
@@ -139,7 +139,7 @@ undoing on holes cannot make holes re-appear.
 
 \(fn &optional ARG)" t nil)
 
-(autoload (quote holes-abbrev-complete) "holes" "\
+(autoload 'holes-abbrev-complete "holes" "\
 Complete abbrev by putting holes and indenting.
 Moves point at beginning of expanded text.  Put this function as
 call-back for your abbrevs, and just expanded \"#\" and \"@{..}\" will
@@ -147,7 +147,7 @@ become holes.
 
 \(fn)" nil nil)
 
-(autoload (quote holes-insert-and-expand) "holes" "\
+(autoload 'holes-insert-and-expand "holes" "\
 Insert S, expand it and replace #s and @{]s by holes.
 
 \(fn S)" nil nil)
@@ -155,10 +155,10 @@ Insert S, expand it and replace #s and @{]s by holes.
 ;;;***
 
 ;;;### (autoloads (maths-menu-mode) "maths-menu" "../lib/maths-menu.el"
-;;;;;;  (19107 62723))
+;;;;;;  (19110 10300))
 ;;; Generated autoloads from ../lib/maths-menu.el
 
-(autoload (quote maths-menu-mode) "maths-menu" "\
+(autoload 'maths-menu-mode "maths-menu" "\
 Install a menu for entering mathematical characters.
 Uses window system menus only when they can display multilingual text.
 Otherwise the menu-bar item activates the text-mode menu system.
@@ -169,16 +169,16 @@ 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" (19107 62126))
+;;;;;;  "pg-assoc" "pg-assoc.el" (19110 10300))
 ;;; Generated autoloads from pg-assoc.el
 
-(autoload (quote proof-associated-buffers) "pg-assoc" "\
+(autoload '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" "\
+(autoload 'proof-associated-windows "pg-assoc" "\
 Return a list of the associated buffers windows.
 Dead or nil buffers are not represented in the list.
 
@@ -187,10 +187,10 @@ Dead or nil buffers are not represented in the list.
 ;;;***
 
 ;;;### (autoloads (proof-goals-config-done) "pg-goals" "pg-goals.el"
-;;;;;;  (19107 49109))
+;;;;;;  (19110 10300))
 ;;; Generated autoloads from pg-goals.el
 
-(autoload (quote proof-goals-config-done) "pg-goals" "\
+(autoload 'proof-goals-config-done "pg-goals" "\
 Initialise the goals buffer after the child has been configured.
 
 \(fn)" nil nil)
@@ -198,21 +198,21 @@ 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" (19108 51632))
+;;;;;;  "pg-pgip" "pg-pgip.el" (19110 13559))
 ;;; Generated autoloads from pg-pgip.el
 
-(autoload 'pg-pgip-process-packet "pg-pgip" "\
+(autoload (quote pg-pgip-process-packet) "pg-pgip" "\
 Process the command packet PGIP, which is parsed XML according to pg-xml-parse-*.
 The list PGIPS may contain one or more PGIP packets, whose contents are processed.
 
 \(fn PGIPS)" nil nil)
 
-(autoload 'pg-pgip-maybe-askpgip "pg-pgip" "\
+(autoload (quote pg-pgip-maybe-askpgip) "pg-pgip" "\
 Send an <askpgip> message to the prover if PGIP is supported.
 
 \(fn)" nil nil)
 
-(autoload 'pg-pgip-askprefs "pg-pgip" "\
+(autoload (quote pg-pgip-askprefs) "pg-pgip" "\
 Send an <askprefs> message to the prover.
 
 \(fn)" nil nil)
@@ -220,9 +220,9 @@ Send an <askprefs> message to the prover.
 ;;;***
 
 ;;;### (autoloads (pg-response-has-error-location proof-next-error
-;;;;;;  pg-response-display-with-face pg-response-maybe-erase proof-response-config-done
-;;;;;;  proof-response-mode) "pg-response" "pg-response.el" (19107
-;;;;;;  62473))
+;;;;;;  pg-response-message pg-response-display-with-face pg-response-maybe-erase
+;;;;;;  proof-response-config-done proof-response-mode) "pg-response"
+;;;;;;  "pg-response.el" (19112 23312))
 ;;; Generated autoloads from pg-response.el
 
 (autoload (quote proof-response-mode) "pg-response" "\
@@ -251,10 +251,14 @@ Returns non-nil if response buffer was cleared.
 
 (autoload (quote pg-response-display-with-face) "pg-response" "\
 Display STR with FACE in response buffer.
-Also updates `proof-shell-last-output'.
 
 \(fn STR &optional FACE)" nil nil)
 
+(autoload (quote pg-response-message) "pg-response" "\
+Issue the message ARGS in the response buffer and display it.
+
+\(fn &rest ARGS)" nil nil)
+
 (autoload (quote proof-next-error) "pg-response" "\
 Jump to location of next error reported in the response buffer.
 
@@ -275,10 +279,10 @@ See `pg-next-error-regexp'.
 ;;;***
 
 ;;;### (autoloads (pg-defthymode) "pg-thymodes" "pg-thymodes.el"
-;;;;;;  (19107 62476))
+;;;;;;  (19110 10300))
 ;;; Generated autoloads from pg-thymodes.el
 
-(autoload (quote pg-defthymode) "pg-thymodes" "\
+(autoload 'pg-defthymode "pg-thymodes" "\
 Define a Proof General mode for theory files.
 Mode name is SYM-mode, named NAMED.  BODY is the body of a setq and
 can define a number of variables for the mode, viz:
@@ -300,10 +304,24 @@ All of these settings are optional.
 ;;;;;;  pg-previous-matching-input-from-input 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-terminator-enable
-;;;;;;  proof-define-assistant-command-witharg proof-define-assistant-command)
-;;;;;;  "pg-user" "pg-user.el" (19108 51656))
+;;;;;;  proof-define-assistant-command-witharg proof-define-assistant-command
+;;;;;;  proof-goto-point proof-script-new-command-advance) "pg-user"
+;;;;;;  "pg-user.el" (19110 10300))
 ;;; Generated autoloads from pg-user.el
 
+(autoload 'proof-script-new-command-advance "pg-user" "\
+Move point to a nice position for a new command.
+Assumes that point is at the end of a command.
+
+\(fn)" t nil)
+
+(autoload 'proof-goto-point "pg-user" "\
+Assert or retract to the command at current position.
+Calls `proof-assert-until-point' or `proof-retract-until-point' as
+appropriate.
+
+\(fn)" t nil)
+
 (autoload 'proof-define-assistant-command "pg-user" "\
 Define FN (docstring DOC) to send BODY to prover, based on CMDVAR.
 BODY defaults to CMDVAR, a variable.
@@ -394,8 +412,8 @@ Not documented
 
 ;;;***
 
-;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (19108
-;;;;;;  51674))
+;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (19110
+;;;;;;  10300))
 ;;; Generated autoloads from pg-xml.el
 
 (autoload 'pg-xml-parse-string "pg-xml" "\
@@ -406,7 +424,7 @@ 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" (19108 51693))
+;;;;;;  "proof-depends" "proof-depends.el" (19110 10300))
 ;;; Generated autoloads from proof-depends.el
 
 (autoload 'proof-depends-process-dependencies "proof-depends" "\
@@ -424,7 +442,7 @@ Make a portion of a context-sensitive menu showing proof dependencies.
 ;;;***
 
 ;;;### (autoloads (proof-easy-config) "proof-easy-config" "proof-easy-config.el"
-;;;;;;  (19108 4440))
+;;;;;;  (19110 10300))
 ;;; Generated autoloads from proof-easy-config.el
 
 (autoload 'proof-easy-config "proof-easy-config" "\
@@ -437,7 +455,7 @@ the `proof-assistant-table', which see.
 ;;;***
 
 ;;;### (autoloads (proof-indent-line) "proof-indent" "proof-indent.el"
-;;;;;;  (19106 28181))
+;;;;;;  (19110 10300))
 ;;; Generated autoloads from proof-indent.el
 
 (autoload 'proof-indent-line "proof-indent" "\
@@ -448,7 +466,7 @@ Indent current line of proof script, if indentation enabled.
 ;;;***
 
 ;;;### (autoloads (proof-maths-menu-enable proof-maths-menu-set-global)
-;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (19106 28181))
+;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (19110 10300))
 ;;; Generated autoloads from proof-maths-menu.el
 
 (autoload 'proof-maths-menu-set-global "proof-maths-menu" "\
@@ -468,55 +486,35 @@ 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" (19108 51708))
+;;;### (autoloads (proof-aux-menu proof-menu-define-specific proof-menu-define-main
+;;;;;;  proof-menu-define-keys) "proof-menu" "proof-menu.el" (19112
+;;;;;;  23313))
 ;;; Generated autoloads from proof-menu.el
 
-(autoload 'proof-menu-define-keys "proof-menu" "\
-Not documented
+(autoload (quote proof-menu-define-keys) "proof-menu" "\
+Prover specific keymap under C-c C-a.
 
 \(fn MAP)" nil nil)
 
-(autoload 'proof-menu-define-main "proof-menu" "\
+(autoload (quote proof-menu-define-main) "proof-menu" "\
 Not documented
 
 \(fn)" nil nil)
 
-(autoload 'proof-menu-define-specific "proof-menu" "\
+(autoload (quote proof-menu-define-specific) "proof-menu" "\
 Not documented
 
 \(fn)" nil nil)
 
-(autoload 'proof-aux-menu "proof-menu" "\
+(autoload (quote proof-aux-menu) "proof-menu" "\
 Construct and return PG auxiliary menu used in non-scripting buffers.
 
 \(fn)" nil nil)
 
-(autoload 'proof-defpacustom-fn "proof-menu" "\
-As for macro `defpacustom' but evaluating arguments.
-
-\(fn NAME VAL ARGS)" nil nil)
-
-(autoload 'defpacustom "proof-menu" "\
-Define a setting NAME for the current proof assitant, default VAL.
-NAME can correspond to some internal setting, flag, etc, for the
-proof assistant, in which case a :setting and :type value should be provided.
-The :type of NAME should be one of 'integer, 'boolean, 'string.
-The customization variable is automatically in group `proof-assistant-setting'.
-The function `proof-assistant-format' is used to format VAL.
-If NAME corresponds instead to a PG internal setting, then a form :eval to
-evaluate can be provided instead.
-
-\(fn NAME VAL &rest ARGS)" nil (quote macro))
-
-;;;***
-
-
 ;;;***
 
 ;;;### (autoloads (proof-mmm-enable proof-mmm-set-global) "proof-mmm"
-;;;;;;  "proof-mmm.el" (19109 31675))
+;;;;;;  "proof-mmm.el" (19110 10300))
 ;;; Generated autoloads from proof-mmm.el
 
 (autoload 'proof-mmm-set-global "proof-mmm" "\
@@ -536,64 +534,81 @@ in future if we have just activated it for this buffer.
 ;;;***
 
 ;;;### (autoloads (proof-config-done proof-mode proof-insert-sendback-command
-;;;;;;  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-colour-locked) "proof-script" "proof-script.el" (19108
-;;;;;;  51751))
+;;;;;;  proof-insert-pbp-command proof-register-possibly-new-processed-file
+;;;;;;  pg-set-span-helphighlights proof-locked-region-empty-p proof-locked-region-full-p
+;;;;;;  proof-locked-end proof-unprocessed-begin proof-colour-locked)
+;;;;;;  "proof-script" "proof-script.el" (19112 23313))
 ;;; Generated autoloads from proof-script.el
 
-(autoload 'proof-colour-locked "proof-script" "\
+(autoload (quote proof-colour-locked) "proof-script" "\
 Alter the colour of the locked region according to variable `proof-colour-locked'.
 
 \(fn)" t nil)
 
-(autoload 'proof-unprocessed-begin "proof-script" "\
+(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 'proof-locked-end "proof-script" "\
+(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 'proof-locked-region-full-p "proof-script" "\
+(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 'proof-locked-region-empty-p "proof-script" "\
+(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 'pg-set-span-helphighlights "proof-script" "\
+(autoload (quote pg-set-span-helphighlights) "proof-script" "\
 Add a daughter help span for SPAN with help message, highlight, actions.
 We add the last output (which should be non-empty) to the hover display here.
 Optional argument NOHIGHLIGHT means do not add highlight mouse face property.
+Argumen FACE means add face property FACE.
 
-\(fn SPAN &optional NOHIGHLIGHT)" nil nil)
+\(fn SPAN &optional NOHIGHLIGHT FACE)" nil nil)
 
-(autoload 'proof-insert-pbp-command "proof-script" "\
+(autoload (quote proof-register-possibly-new-processed-file) "proof-script" "\
+Register a possibly new FILE as having been processed by the prover.
+
+If INFORMPROVER is non-nil, the proof assistant will be told about this,
+to co-ordinate with its internal file-management.  (Otherwise we assume
+that it is a message from the proof assistant which triggers this call).
+In this case, the user will be queried to save some buffers, unless
+NOQUESTIONS is non-nil.
+
+No action is taken if the file is already registered.
+
+A warning message is issued if the register request came from the
+proof assistant and Emacs has a modified buffer visiting the file.
+
+\(fn FILE &optional INFORMPROVER NOQUESTIONS)" nil nil)
+
+(autoload (quote proof-insert-pbp-command) "proof-script" "\
 Insert CMD into the proof queue.
 
 \(fn CMD)" nil nil)
 
-(autoload 'proof-insert-sendback-command "proof-script" "\
+(autoload (quote proof-insert-sendback-command) "proof-script" "\
 Insert CMD into the proof script, execute assert-until-point.
 
 \(fn CMD)" nil nil)
 
-(autoload 'proof-mode "proof-script" "\
+(autoload (quote proof-mode) "proof-script" "\
 Proof General major mode class for proof scripts.
 \\{proof-mode-map}
 
 \(fn)" t nil)
 
-(autoload 'proof-config-done "proof-script" "\
+(autoload (quote proof-config-done) "proof-script" "\
 Finish setup of Proof General scripting mode.
 Call this function in the derived mode for the proof assistant to
 finish setup which depends on specific proof assistant configuration.
@@ -606,10 +621,10 @@ 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-ready-prover) "proof-shell"
-;;;;;;  "proof-shell.el" (19108 51779))
+;;;;;;  "proof-shell.el" (19112 23489))
 ;;; Generated autoloads from proof-shell.el
 
-(autoload 'proof-shell-ready-prover "proof-shell" "\
+(autoload (quote proof-shell-ready-prover) "proof-shell" "\
 Make sure the proof assistant is ready for a command.
 If QUEUEMODE is set, succeed if the proof shell is busy but
 has mode QUEUEMODE, which is a symbol or list of symbols.
@@ -621,13 +636,13 @@ No change to current buffer or point.
 (defsubst proof-shell-live-buffer nil "\
 Return buffer of active proof assistant, or nil if none running." (and proof-shell-buffer (buffer-live-p proof-shell-buffer) (scomint-check-proc proof-shell-buffer)))
 
-(autoload 'proof-shell-available-p "proof-shell" "\
+(autoload (quote proof-shell-available-p) "proof-shell" "\
 Return non-nil if there is a proof shell active and available.
 No error messages.  Useful as menu or toolbar enabler.
 
 \(fn)" nil nil)
 
-(autoload 'proof-shell-insert "proof-shell" "\
+(autoload (quote proof-shell-insert) "proof-shell" "\
 Insert STRING at the end of the proof shell, call `scomint-send-input'.
 
 First we call `proof-shell-insert-hook'.  The arguments `action' and
@@ -648,7 +663,7 @@ used in `proof-append-alist' when we start processing a queue, and in
 
 \(fn STRING ACTION &optional SCRIPTSPAN)" nil nil)
 
-(autoload 'proof-start-queue "proof-shell" "\
+(autoload (quote proof-start-queue) "proof-shell" "\
 Begin processing a queue of commands in ALIST.
 If START is non-nil, START and END are buffer positions in the
 active scripting buffer for the queue region.
@@ -657,7 +672,7 @@ This function calls `proof-append-alist'.
 
 \(fn START END ALIST)" nil nil)
 
-(autoload 'proof-extend-queue "proof-shell" "\
+(autoload (quote proof-extend-queue) "proof-shell" "\
 Extend the current queue with commands in ALIST, queue end END.
 To make sense, the commands should correspond to processing actions
 for processing a region from (buffer-queue-or-locked-end) to END.
@@ -665,7 +680,7 @@ The queue mode is set to 'advancing
 
 \(fn END ALIST)" nil nil)
 
-(autoload 'proof-shell-wait "proof-shell" "\
+(autoload (quote proof-shell-wait) "proof-shell" "\
 Busy wait for `proof-shell-busy' to become nil.
 Needed between sequences of commands to maintain synchronization,
 because Proof General does not allow for the action list to be extended
@@ -673,7 +688,7 @@ in some cases.   May be called by `proof-shell-invisible-command'.
 
 \(fn)" nil nil)
 
-(autoload 'proof-shell-invisible-command "proof-shell" "\
+(autoload (quote proof-shell-invisible-command) "proof-shell" "\
 Send CMD to the proof process.
 The CMD is `invisible' in the sense that it is not recorded in buffer.
 CMD may be a string or a string-yielding expression.
@@ -695,7 +710,7 @@ If NOERROR is set, surpress usual error action.
 
 \(fn CMD &optional WAIT INVISIBLECALLBACK &rest FLAGS)" nil nil)
 
-(autoload 'proof-shell-invisible-cmd-get-result "proof-shell" "\
+(autoload (quote proof-shell-invisible-cmd-get-result) "proof-shell" "\
 Execute CMD and return result as a string.
 This expects CMD to result in some theorem prover output.
 Ordinary output (and error handling) is disabled, and the result
@@ -703,18 +718,18 @@ Ordinary output (and error handling) is disabled, and the result
 
 \(fn CMD)" nil nil)
 
-(autoload 'proof-shell-invisible-command-invisible-result "proof-shell" "\
+(autoload (quote proof-shell-invisible-command-invisible-result) "proof-shell" "\
 Execute CMD for side effect in the theorem prover, waiting before and after.
 Error messages are displayed as usual.
 
 \(fn CMD)" nil nil)
 
-(autoload 'proof-shell-mode "proof-shell" "\
+(autoload (quote proof-shell-mode) "proof-shell" "\
 Proof General shell mode class for proof assistant processes
 
 \(fn)" t nil)
 
-(autoload 'proof-shell-config-done "proof-shell" "\
+(autoload (quote proof-shell-config-done) "proof-shell" "\
 Initialise the specific prover after the child has been configured.
 Every derived shell mode should call this function at the end of
 processing.
@@ -724,7 +739,7 @@ processing.
 ;;;***
 
 ;;;### (autoloads (proof-ready-for-assistant) "proof-site" "proof-site.el"
-;;;;;;  (19108 51789))
+;;;;;;  (19110 10300))
 ;;; Generated autoloads from proof-site.el
 
 (autoload 'proof-ready-for-assistant "proof-site" "\
@@ -736,7 +751,7 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'.
 ;;;***
 
 ;;;### (autoloads (proof-splash-message proof-splash-display-screen)
-;;;;;;  "proof-splash" "proof-splash.el" (19108 55485))
+;;;;;;  "proof-splash" "proof-splash.el" (19110 10300))
 ;;; Generated autoloads from proof-splash.el
 
 (autoload 'proof-splash-display-screen "proof-splash" "\
@@ -753,7 +768,7 @@ Make sure the user gets welcomed one way or another.
 ;;;***
 
 ;;;### (autoloads (proof-splice-separator proof-format) "proof-syntax"
-;;;;;;  "proof-syntax.el" (19107 64438))
+;;;;;;  "proof-syntax.el" (19112 23313))
 ;;; Generated autoloads from proof-syntax.el
 
 (autoload (quote proof-format) "proof-syntax" "\
@@ -771,13 +786,13 @@ Splice SEP into list of STRINGS, ignoring nil entries.
 ;;;***
 
 ;;;### (autoloads (proof-toolbar-scripting-menu proof-toolbar-setup)
-;;;;;;  "proof-toolbar" "proof-toolbar.el" (19107 64554))
+;;;;;;  "proof-toolbar" "proof-toolbar.el" (19112 23313))
 ;;; Generated autoloads from proof-toolbar.el
 
 (autoload (quote proof-toolbar-setup) "proof-toolbar" "\
-Initialize Proof General toolbar and enable it for current buffer.
-If `proof-toolbar-enable' is nil, change the current buffer toolbar
-to the default toolbar.
+Initialize Proof General toolbar and enable it for all PG buffers.
+If `proof-toolbar-enable' is nil, change the buffer toolbars
+back the default toolbar.
 
 \(fn)" t nil)
  (autoload 'proof-toolbar-toggle "proof-toolbar")
@@ -789,22 +804,16 @@ Menu made from the Proof General toolbar commands.
 
 ;;;***
 
-;;;### (autoloads (proof-unicode-tokens-set-global proof-unicode-tokens-enable)
-;;;;;;  "proof-unicode-tokens" "proof-unicode-tokens.el" (19106 28182))
+;;;### (autoloads (proof-unicode-tokens-set-global proof-unicode-tokens-mode-if-enabled)
+;;;;;;  "proof-unicode-tokens" "proof-unicode-tokens.el" (19112 23355))
 ;;; Generated autoloads from proof-unicode-tokens.el
 
-(autoload 'proof-unicode-tokens-enable "proof-unicode-tokens" "\
-Turn on or off Unicode tokens mode in Proof General script buffer.
-This invokes `unicode-tokens-mode' to toggle the setting for the current
-buffer, and then sets PG's option for default to match.
-Also we arrange to have unicode tokens mode turn itself on automatically
-in future if we have just activated it for this buffer.
-Note: this function is called when the customize setting for the prover
-is changed.
+(autoload (quote proof-unicode-tokens-mode-if-enabled) "proof-unicode-tokens" "\
+Turn on or off the Unicode Tokens minor mode in this buffer.
 
-\(fn)" t nil)
+\(fn)" nil nil)
 
-(autoload 'proof-unicode-tokens-set-global "proof-unicode-tokens" "\
+(autoload (quote proof-unicode-tokens-set-global) "proof-unicode-tokens" "\
 Set global status of unicode tokens mode for PG buffers to be FLAG.
 Turn on/off menu in all script buffers and ensure new buffers follow suit.
 
@@ -812,8 +821,31 @@ Turn on/off menu in all script buffers and ensure new buffers follow suit.
 
 ;;;***
 
+;;;### (autoloads (defpacustom proof-defpacustom-fn) "proof-utils"
+;;;;;;  "proof-utils.el" (19112 23313))
+;;; Generated autoloads from proof-utils.el
+
+(autoload (quote proof-defpacustom-fn) "proof-utils" "\
+As for macro `defpacustom' but evaluating arguments.
+
+\(fn NAME VAL ARGS)" nil nil)
+
+(autoload (quote defpacustom) "proof-utils" "\
+Define a setting NAME for the current proof assitant, default VAL.
+NAME can correspond to some internal setting, flag, etc, for the
+proof assistant, in which case a :setting and :type value should be provided.
+The :type of NAME should be one of 'integer, 'boolean, 'string.
+The customization variable is automatically in group `proof-assistant-setting'.
+The function `proof-assistant-format' is used to format VAL.
+If NAME corresponds instead to a PG internal setting, then a form :eval to
+evaluate can be provided instead.
+
+\(fn NAME VAL &rest ARGS)" nil (quote macro))
+
+;;;***
+
 ;;;### (autoloads (scomint-make scomint-make-in-buffer) "scomint"
-;;;;;;  "../lib/scomint.el" (19109 20818))
+;;;;;;  "../lib/scomint.el" (19110 10300))
 ;;; Generated autoloads from ../lib/scomint.el
 
 (autoload 'scomint-make-in-buffer "scomint" "\
@@ -845,10 +877,10 @@ If PROGRAM is a string, any more args are arguments to PROGRAM.
 ;;;***
 
 ;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "../lib/texi-docstring-magic.el"
-;;;;;;  (19107 62790))
+;;;;;;  (19110 10300))
 ;;; Generated autoloads from ../lib/texi-docstring-magic.el
 
-(autoload (quote texi-docstring-magic) "texi-docstring-magic" "\
+(autoload 'texi-docstring-magic "texi-docstring-magic" "\
 Update all texi docstring magic annotations in buffer.
 With prefix arg, no errors on unknown symbols.  (This results in
 @def .. @end being deleted if not known).
@@ -858,10 +890,10 @@ With prefix arg, no errors on unknown symbols.  (This results in
 ;;;***
 
 ;;;### (autoloads (unicode-chars-list-chars) "unicode-chars" "../lib/unicode-chars.el"
-;;;;;;  (19107 62795))
+;;;;;;  (19110 10300))
 ;;; Generated autoloads from ../lib/unicode-chars.el
 
-(autoload (quote unicode-chars-list-chars) "unicode-chars" "\
+(autoload 'unicode-chars-list-chars "unicode-chars" "\
 Insert each Unicode character into a buffer.
 Lets you see which characters are available for literal display
 in your emacs font.
@@ -871,10 +903,10 @@ in your emacs font.
 ;;;***
 
 ;;;### (autoloads (unicode-tokens-encode-str) "unicode-tokens" "../lib/unicode-tokens.el"
-;;;;;;  (19108 51332))
+;;;;;;  (19112 23313))
 ;;; Generated autoloads from ../lib/unicode-tokens.el
 
-(autoload 'unicode-tokens-encode-str "unicode-tokens" "\
+(autoload (quote unicode-tokens-encode-str) "unicode-tokens" "\
 Return a unicode encoded version presentation of STR.
 
 \(fn STR)" nil nil)
@@ -885,7 +917,7 @@ Return a unicode encoded version presentation of STR.
 ;;;;;;  "../lib/pg-fontsets.el" "../lib/proof-compat.el" "../lib/span.el"
 ;;;;;;  "pg-autotest.el" "pg-custom.el" "pg-pbrpm.el" "pg-vars.el"
 ;;;;;;  "proof-auxmodes.el" "proof-config.el" "proof-faces.el" "proof-useropts.el"
-;;;;;;  "proof-utils.el" "proof.el") (19109 31686 18792))
+;;;;;;  "proof.el" "test.el") (19112 23608 594193))
 
 ;;;***
 
diff --git a/generic/proof-auxmodes.el b/generic/proof-auxmodes.el
index f4f2a60f..e29bc753 100644
--- a/generic/proof-auxmodes.el
+++ b/generic/proof-auxmodes.el
@@ -11,7 +11,6 @@
 ;;
 
 (require 'proof-utils)			; proof-ass, proof-eval...
-(require 'proof-autoloads)		; aux mode functions autoloaded
 
 ;;; Code:
 
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 5a373493..360581b9 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -70,7 +70,8 @@
 
 (require 'proof-useropts)		; user options
 (require 'proof-faces)			; user options: faces
-
+(eval-when-compile
+  (require 'custom))
 
 ;;
 ;; Prelude
diff --git a/generic/proof-maths-menu.el b/generic/proof-maths-menu.el
index de02cc7a..fdc1f7e0 100644
--- a/generic/proof-maths-menu.el
+++ b/generic/proof-maths-menu.el
@@ -19,11 +19,11 @@
 ;;
 
 (eval-when-compile
-  (require 'proof-utils) ; for proof-ass, proof-eval-when-ready-for-assistant
   (require 'cl))
 
 (eval-when (compile)
-  (require 'maths-menu)) ; it's loaded dynamically at runtime
+  (require 'proof-auxmodes)	  ; loaded by proof.el
+  (require 'maths-menu))	  ; loaded dynamically in proof-auxmodes
 
 
 ;;;###autoload
diff --git a/generic/proof-mmm.el b/generic/proof-mmm.el
index 96ba5847..ce0dd1ef 100644
--- a/generic/proof-mmm.el
+++ b/generic/proof-mmm.el
@@ -22,14 +22,11 @@
 ;; It should define an MMM submode class called <foo>.
 
 (eval-when-compile
-  (require 'proof-utils) ; for proof-ass, proof-eval-when-ready-for-assistant
   (require 'cl))
 
 (eval-when (compile)
-   (require 'proof-auxmodes) ; it will have been loaded
-   (require 'mmm-auto))  ; it's loaded dynamically at runtime
-
-(require 'proof-site)
+  (require 'proof-auxmodes)	  ; will be loaded
+  (require 'mmm-auto))		  ; loaded dynamically by proof-auxmodes
 
 ;; The following function is called by the menu item for MMM-Mode.  It
 ;; is an attempt at an intuitive behaviour without confusing the user
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index ba28c3a5..fc23aabd 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -1,6 +1,6 @@
 ;;; proof-toolbar.el --- Toolbar for Proof General
 ;;
-;; Copyright (C) 1998-2008  David Aspinall / LFCS.
+;; Copyright (C) 1998-2009  David Aspinall / LFCS.
 ;; Author:    David Aspinall <David.Aspinall@ed.ac.uk>
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -23,8 +23,8 @@
 (eval-and-compile
   (require 'span)
   (require 'proof-utils)
-  (require 'proof-config)
-  (require 'proof-autoloads))
+  (require 'proof-config))
+
 
 ;;
 ;; Function, icon, button names
diff --git a/generic/proof-unicode-tokens.el b/generic/proof-unicode-tokens.el
index 5c3fd91d..270309ed 100644
--- a/generic/proof-unicode-tokens.el
+++ b/generic/proof-unicode-tokens.el
@@ -19,12 +19,14 @@
 ;;; Code:
 
 (eval-when-compile
-  (require 'proof-utils) ; for proof-ass, proof-eval-when-ready-for-assistant
-  (require 'scomint)	 ; scomint-check-proc
   (require 'cl))
 
 (eval-when (compile)
-  (require 'unicode-tokens)) ; it's loaded dynamically at runtime
+    (require 'scomint)
+    (require 'proof-auxmodes)	 ; loaded by proof.el, autoloads us
+    (require 'unicode-tokens))	 ; it will be loaded by proof-auxmodes
+
+(require 'proof-config)			; config variables
 
 (defvar proof-unicode-tokens-initialised nil
   "Flag indicating whether or not we've performed startup.")
@@ -55,20 +57,6 @@
 
 
 ;;;###autoload
-(defun proof-unicode-tokens-enable ()
-  "Turn on or off Unicode tokens mode in Proof General script buffer.
-This invokes `unicode-tokens-mode' to toggle the setting for the current
-buffer, and then sets PG's option for default to match.
-Also we arrange to have unicode tokens mode turn itself on automatically
-in future if we have just activated it for this buffer.
-Note: this function is called when the customize setting for the prover
-is changed."
-  (interactive)
-  (when (proof-unicode-tokens-support-available) ;; loads unicode-tokens
-    (unless proof-unicode-tokens-initialised
-      (proof-unicode-tokens-init))
-    (proof-unicode-tokens-set-global (not unicode-tokens-mode))))
-
 (defun proof-unicode-tokens-mode-if-enabled ()
   "Turn on or off the Unicode Tokens minor mode in this buffer."
   (unicode-tokens-mode
@@ -89,6 +77,22 @@ Turn on/off menu in all script buffers and ensure new buffers follow suit."
    (unicode-tokens-mode (if flag 1 0)))
   (proof-unicode-tokens-configure-prover))
 
+(defun proof-unicode-tokens-enable ()
+  "Turn on or off Unicode tokens mode in Proof General script buffer.
+This invokes `unicode-tokens-mode' to toggle the setting for the current
+buffer, and then sets PG's option for default to match.
+Also we arrange to have unicode tokens mode turn itself on automatically
+in future if we have just activated it for this buffer.
+Note: this function is called when the customize setting for the prover
+is changed."
+  (interactive)
+  (when (proof-unicode-tokens-support-available) ;; loads unicode-tokens
+    (unless proof-unicode-tokens-initialised
+      (proof-unicode-tokens-init))
+    (with-no-warnings ; spurious warning on `proof-unicode-tokens-set-global'
+      (proof-unicode-tokens-set-global (not unicode-tokens-mode)))))
+
+
 ;;;
 ;;; Interface to custom to dynamically change tables (via proof-set-value)
 ;;;
diff --git a/generic/proof.el b/generic/proof.el
index a00c6d8a..9ec58d03 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -23,14 +23,16 @@
 ;;; Code:
 
 (require 'proof-site)			; site/prover config, global vars, autoloads
-(require 'proof-compat)			; Emacs and OS compatibility
-(require 'proof-utils)			; utilities
-(require 'proof-config)			; configuration variables
 
 (unless noninteractive
   (proof-splash-message))		; welcome the user now.
 
-(require 'proof-auxmodes)		; Further autoloads
+(require 'proof-compat)			; Emacs and OS compatibility
+(require 'proof-utils)			; utilities
+(require 'proof-config)			; configuration variables
+(require 'proof-auxmodes)		; auxmode functions
+(require 'proof-script)			; script mode
+(require 'proof-shell)			; shell mode
 
 (provide 'proof)
 ;;; proof.el ends here