Fixup loading.

5 files changed, 22 insertions, 5 deletions

diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 2363e248..8782d2c8 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -15,7 +15,7 @@ Indent current line of proof script" t nil)
 
 ;;;***
 
-;;;### (autoloads (proof-menu-define-specific proof-menu-define-main proof-menu-define-keys) "proof-menu" "generic/proof-menu.el")
+;;;### (autoloads (proof-deftoggle proof-menu-define-specific proof-menu-define-main proof-menu-define-keys) "proof-menu" "generic/proof-menu.el")
 
 (autoload 'proof-menu-define-keys "proof-menu" nil nil nil)
 
@@ -23,6 +23,10 @@ Indent current line of proof script" t nil)
 
 (autoload 'proof-menu-define-specific "proof-menu" nil nil nil)
 
+(autoload 'proof-deftoggle "proof-menu" "\
+Define a function VAR-toggle for toggling a boolean customize setting VAR.
+The toggle function uses customize-set-variable to change the variable." nil 'macro)
+
 ;;;***
 
 ;;;### (autoloads nil "proof-script" "generic/proof-script.el")
@@ -76,8 +80,7 @@ If WAIT is an integer, wait for that many seconds afterwards." nil nil)
 ;;;### (autoloads (proof-splash-display-screen) "proof-splash" "generic/proof-splash.el")
 
 (autoload 'proof-splash-display-screen "proof-splash" "\
-Save window config and display Proof General splash screen.
-Only do it if proof-splash-enable is non-nil." nil nil)
+Save window config and display Proof General splash screen." nil nil)
 
 ;;;***
 
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 6c392faa..a2a390a9 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -117,6 +117,8 @@ It was constructed with the macro proof-customize-toggle.")
 
 ;; FIXME: combine this with above, and remove messing calls in
 ;; proof-script.
+;; This is autoloaded for some specific PAs to define commands.
+;;;###autoload
 (defmacro proof-deftoggle (var)
   "Define a function VAR-toggle for toggling a boolean customize setting VAR.
 The toggle function uses customize-set-variable to change the variable."
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 5ea44dda..15275c28 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2321,6 +2321,7 @@ sent to the assistant."
 ;;
 
 (eval-and-compile			; to define vars
+;;; NB: autoload tag below doesn't work
 ;;;###autoload
 (define-derived-mode proof-mode fundamental-mode 
   proof-general-name
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 4df2d1ab..f062cec3 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -278,8 +278,6 @@ Note: to change proof assistant, you must start a new Emacs session.")
 (defconst proof-general-version "Proof General Version 3.2pre000505. Released by da."
  "Version string identifying Proof General release.")
 
-(require 'proof-autoloads)		; PG autoloads.
-
 (provide 'proof-site))
 
 ;; proof-site.el ends here
diff --git a/generic/proof.el b/generic/proof.el
index 0f0964fd..f90b7454 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -11,6 +11,7 @@
 ;;
 
 (require 'proof-site)			; site config
+(require 'proof-autoloads)		; autoloaded functions
 (require 'proof-compat)			; Emacs and OS compatibility
 (require 'proof-utils)			; utilities
 (require 'proof-config)			; configuration variables
@@ -22,6 +23,18 @@
 
 
 ;;;
+;;; Extra autoloads that aren't automatic 
+;;; (defined with define-derived-mode)
+;;;
+
+(autoload 'proof-mode "proof-script"
+  "Proof General major mode class for proof scripts.")
+
+(autoload 'proof-shell-mode "proof-shell"
+  "Proof General shell mode class for proof assistant processes")
+
+
+;;;
 ;;; Global variables
 ;;;