Improved loading

4 files changed, 14 insertions, 6 deletions

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 8761ff68..9a165804 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -107,6 +107,7 @@ See the functions `proof-start-queue' and `proof-exec-loop'.")
 ;; Maybe proof-shell-ready-prover doesn't need to start the shell?
 ;;
 
+;;;###autoload
 (defun proof-shell-ready-prover (&optional queuemode)
   "Make sure the proof assistant is ready for a command.
 If QUEUEMODE is set, succeed if the proof shell is busy but
@@ -117,12 +118,14 @@ No change to current buffer or point."
   (unless (or (not proof-shell-busy) (eq queuemode proof-shell-busy))
     (error "Proof Process Busy!")))
 
+;;;###autoload
 (defun proof-shell-live-buffer ()
   "Return buffer of active proof assistant, or nil if none running."
   (and proof-shell-buffer
        (comint-check-proc proof-shell-buffer)
        (buffer-live-p proof-shell-buffer)))
 
+;;;###autoload
 (defun proof-shell-available-p ()
   "Returns non-nil if there is a proof shell active and available.
 No error messages.  Useful as menu or toolbar enabler."
@@ -1176,7 +1179,8 @@ being processed."
 		  (nconc proof-action-list alist))
 	    ;; Really start things going here
 	    (proof-shell-insert (nth 1 item) (nth 2 item)))))))
-    
+
+;;;###autoload    
 (defun proof-start-queue (start end alist)
   "Begin processing a queue of commands in ALIST.
 If START is non-nil, START and END are buffer positions in the
@@ -1187,6 +1191,7 @@ This function calls `proof-append-alist'."
       (proof-set-queue-endpoints start end))
   (proof-append-alist alist))
 
+;;;###autoload
 (defun proof-extend-queue (end alist)
   "Extend the current queue with commands in ALIST, queue end END.
 To make sense, the commands should correspond to processing actions
@@ -1706,6 +1711,7 @@ XEmacs only."
 ;; proof-shell-invisible-command: used to implement user-level commands.
 ;;
 
+;;;###autoload
 (defun proof-shell-wait (&optional timeout)
   "Busy wait for proof-shell-busy to become nil, or for TIMEOUT seconds.
 Needed between sequences of commands to maintain synchronization,
@@ -1758,6 +1764,7 @@ Calls proof-state-change-hook."
 ; Other (sensible) possibility is to call
 ; proof-shell-handle-error-or-interrupt-hook with span as argument.
 
+;;;###autoload
 (defun proof-shell-invisible-command (cmd &optional wait)
   "Send CMD to the proof process.  Add terminal string if necessary.
 By default, let the command be processed asynchronously.
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index c4cb9ca0..cd2995b2 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -8,7 +8,8 @@
 ;;
 ;; NB: FSF GNU Emacs has no toolbar facility. This file defines
 ;; proof-toolbar-menu which holds the same commands and is put on the
-;; menubar by proof-toolbar-setup (surprisingly).
+;; menubar by proof-toolbar-setup (perhaps surprisingly).
+;; Could consider moving the generic table stuff to proof-menu now.
 ;;
 ;; Toolbar is just for the scripting buffer, currently.
 ;;
@@ -160,7 +161,7 @@ will work for any proof assistant.")
 (deflocal proof-toolbar-itimer nil
   "itimer for updating the toolbar in the current buffer")
 
-;;; ###autoload
+;;;###autoload
 (defun proof-toolbar-setup ()
   "Initialize Proof General toolbar and enable it for the current buffer.
 If proof-mode-use-toolbar is nil, change the current buffer toolbar
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index 6ebff0ad..cf084146 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -215,7 +215,7 @@ A subroutine of proof-x-symbol-enable."
 ;;  proof-x-symbol-configure:     for goals/response buffer (font lock)
 ;;
 
-;;;### autoload
+;;;###autoload
 (defun proof-x-symbol-mode ()
   "Turn on/off x-symbol mode in current buffer, from proof-x-symbol-enable.
 The X-Symbol minor mode is only useful in buffers where symbol input
@@ -238,7 +238,7 @@ takes place (it isn't used for output-only buffers)."
 		;; contents) have changed. Shouldn't x-symbol do this?
 		(font-lock-fontify-buffer)))))))
 
-;;;#### autoload
+;;;####autoload
 (defun proof-x-symbol-shell-config ()
   "Configure the proof shell for x-symbol, if proof-x-symbol-support<>nil.
 Assumes that the current buffer is the proof shell buffer."
diff --git a/generic/texi-docstring-magic.el b/generic/texi-docstring-magic.el
index 206ac0af..9f1552c6 100644
--- a/generic/texi-docstring-magic.el
+++ b/generic/texi-docstring-magic.el
@@ -315,7 +315,7 @@ Markup as @code{stuff} or @lisp stuff @end lisp."
   "Magic string in a texi buffer expanded into @defopt, or @deffn.")
 
 
-
+;;;###autoload
 (defun texi-docstring-magic ()
   "Update all texi docstring magic annotations in buffer."
   (interactive)