Updated.

2 files changed, 40 insertions, 28 deletions

diff --git a/generic/pg-user.el b/generic/pg-user.el
index f5706d74..1e08b123 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -410,6 +410,7 @@ a proof command."
      (error "Proof General not configured for this: set %s" 
 	    ,(symbol-name var))))
 
+;;;###autoload
 (defmacro proof-define-assistant-command (fn doc cmdvar &optional body)
   "Define command FN to send string BODY to proof assistant, based on CMDVAR.
 BODY defaults to CMDVAR, a variable."
@@ -422,6 +423,7 @@ BODY defaults to CMDVAR, a variable."
      (proof-if-setting-configured ,cmdvar
        (proof-shell-invisible-command ,(or body cmdvar)))))
 
+;;;###autoload
 (defmacro proof-define-assistant-command-witharg (fn doc cmdvar prompt &rest body)
   "Define command FN to prompt for string CMDVAR to proof assistant.
 CMDVAR is a function or string.  Automatically has history."
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 80f83c75..133d95ba 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -7,16 +7,21 @@
 
 ;;;***
 
-;;;### (autoloads (pg-pgip-askprefs pg-pgip-process-packet) "pg-pgip" "generic/pg-pgip.el")
+;;;### (autoloads (pg-pgip-askprefs pg-pgip-maybe-askpgip pg-pgip-process-packet) "pg-pgip" "generic/pg-pgip.el")
 
 (autoload 'pg-pgip-process-packet "pg-pgip" "\
-Process the command packet PGIP, which is parsed XML according to pg-xml-parse-*" nil nil)
+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." nil nil)
 
-(autoload 'pg-pgip-askprefs "pg-pgip" nil nil nil)
+(autoload 'pg-pgip-maybe-askpgip "pg-pgip" "\
+Send an <askpgip> message to the prover if PGIP is supported." nil nil)
+
+(autoload 'pg-pgip-askprefs "pg-pgip" "\
+Send an <askprefs> message to the prover." nil nil)
 
 ;;;***
 
-;;;### (autoloads (proof-next-error) "pg-response" "generic/pg-response.el")
+;;;### (autoloads (pg-response-has-error-location proof-next-error) "pg-response" "generic/pg-response.el")
 
 (autoload 'proof-next-error "pg-response" "\
 Jump to location of next error reported in the response buffer.
@@ -26,6 +31,10 @@ negative means move back to previous error messages.
 Just C-u as a prefix means reparse the error message buffer
 and start at the first error." t nil)
 
+(autoload 'pg-response-has-error-location "pg-response" "\
+Return non-nil if the response buffer has an error location.
+See `pg-next-error-regexp'." nil nil)
+
 ;;;***
 
 ;;;### (autoloads (pg-defthymode) "pg-thymodes" "generic/pg-thymodes.el")
@@ -45,6 +54,14 @@ All of these settings are optional." nil 'macro)
 
 ;;;***
 
+;;;### (autoloads (proof-define-assistant-command-witharg) "pg-user" "generic/pg-user.el")
+
+(autoload 'proof-define-assistant-command-witharg "pg-user" "\
+Define command FN to prompt for string CMDVAR to proof assistant.
+CMDVAR is a function or string.  Automatically has history." nil 'macro)
+
+;;;***
+
 ;;;### (autoloads (pg-xml-parse-string) "pg-xml" "generic/pg-xml.el")
 
 (autoload 'pg-xml-parse-string "pg-xml" "\
@@ -96,6 +113,7 @@ KEY is added onto proof-assistant map." nil 'macro)
 Define function FN to send STRING to proof assistant, optional keydef KEY.
 This is intended for defining proof assistant specific functions.
 STRING is sent using proof-shell-invisible-command, which see.
+STRING may be a string or a function which returns a string.
 KEY is added onto proof-assistant map." nil 'macro)
 
 (autoload 'proof-defpacustom-fn "proof-menu" "\
@@ -106,7 +124,7 @@ 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 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." nil 'macro)
@@ -159,20 +177,24 @@ for processing a region from (buffer-queue-or-locked-end) to END.
 The queue mode is set to 'advancing" nil nil)
 
 (autoload 'proof-shell-wait "proof-shell" "\
-Busy wait for `proof-shell-busy' to become nil, or for TIMEOUT seconds.
+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
 in some cases.   May be called by `proof-shell-invisible-command'." nil nil)
 
 (autoload 'proof-shell-invisible-command "proof-shell" "\
-Send CMD to the proof process.  
-CMD may be a string or a string-yielding function.
+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.
+
 Automatically add proof-terminal-char if necessary, examining
 proof-shell-no-auto-terminate-commands.
+
 By default, let the command be processed asynchronously.
 But if optional WAIT command is non-nil, wait for processing to finish
 before and after sending the command.
-If WAIT is an integer, wait for that many seconds afterwards." nil nil)
+
+In case CMD is (or yields) nil, do nothing." nil nil)
 
 ;;;***
 
@@ -207,24 +229,19 @@ to the default toolbar." t nil)
 
 ;;;***
 
-;;;### (autoloads (proof-x-symbol-config-output-buffer proof-x-symbol-shell-config proof-x-symbol-mode proof-x-symbol-decode-region proof-x-symbol-enable proof-x-symbol-support-maybe-available) "proof-x-symbol" "generic/proof-x-symbol.el")
+;;;### (autoloads (proof-x-symbol-config-output-buffer proof-x-symbol-shell-config proof-x-symbol-enable proof-x-symbol-support-maybe-available) "proof-x-symbol" "generic/proof-x-symbol.el")
 
 (autoload 'proof-x-symbol-support-maybe-available "proof-x-symbol" "\
 A test to see whether x-symbol support may be available." nil nil)
 
 (autoload 'proof-x-symbol-enable "proof-x-symbol" "\
-Turn on or off support for X-Symbol, initializing if necessary.
-Calls proof-x-symbol-toggle-clean-buffers afterwards." nil nil)
+Turn on or off X-Symbol in current Proof General script buffer.
+This invokes `x-symbol-mode' to toggle the setting for the current
+buffer, and then sets PG's option for default to match.
+Also we arrange to have X-Symbol mode turn itself on automatically 
+in future if we have just activated it for this buffer." nil nil)
 
-(autoload 'proof-x-symbol-decode-region "proof-x-symbol" "\
-Call (x-symbol-decode-region START END), if x-symbol support is enabled.
-This converts tokens in the region into X-Symbol characters.
-Return new END value." nil nil)
-
-(autoload 'proof-x-symbol-mode "proof-x-symbol" "\
-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
-takes place (it isn't used for output-only buffers)." t nil)
+(defalias 'proof-x-symbol-decode-region 'x-symbol-decode-region)
 
 (autoload 'proof-x-symbol-shell-config "proof-x-symbol" "\
 Configure the proof shell for x-symbol, if proof-x-symbol-support<>nil.
@@ -234,12 +251,5 @@ Assumes that the current buffer is the proof shell buffer." nil nil)
 Configure the current output buffer (goals/response/trace) for X-Symbol." nil nil)
 
 ;;;***
-
-;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "generic/texi-docstring-magic.el")
-
-(autoload 'texi-docstring-magic "texi-docstring-magic" "\
-Update all texi docstring magic annotations in buffer." t nil)
-
-;;;***
 
 (provide 'proof-autoloads)