Update autoloads

1 files changed, 94 insertions, 81 deletions

diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index fe6ef34a..703258ff 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -7,23 +7,10 @@
 
 ;;;***
 
-;;;### (autoloads (bufhist-mode bufhist-exit bufhist-init) "bufhist"
-;;;;;;  "../lib/bufhist.el" (19106 28183))
+;;;### (autoloads (bufhist-exit bufhist-init bufhist-mode) "bufhist"
+;;;;;;  "../lib/bufhist.el" (19108 53141))
 ;;; Generated autoloads from ../lib/bufhist.el
 
-(autoload 'bufhist-init "bufhist" "\
-Initialise a ring history for the current buffer.
-The history will be read-only unless READWRITE is non-nil.
-For read-only histories, edits to the buffer switch to the latest version.
-The size defaults to `bufhist-ring-size'.
-
-\(fn &optional READWRITE RINGSIZE)" t nil)
-
-(autoload 'bufhist-exit "bufhist" "\
-Stop keeping ring history for current buffer.
-
-\(fn)" t nil)
-
 (autoload 'bufhist-mode "bufhist" "\
 Minor mode retaining an in-memory history of the buffer contents.
 
@@ -37,6 +24,19 @@ Commands:\\<bufhist-minor-mode-map>
 
 \(fn &optional ARG)" t nil)
 
+(autoload 'bufhist-init "bufhist" "\
+Initialise a ring history for the current buffer.
+The history will be read-only unless READWRITE is non-nil.
+For read-only histories, edits to the buffer switch to the latest version.
+The size defaults to `bufhist-ring-size'.
+
+\(fn &optional READWRITE RINGSIZE)" t nil)
+
+(autoload 'bufhist-exit "bufhist" "\
+Stop keeping ring history for current buffer.
+
+\(fn)" t nil)
+
 ;;;***
 
 ;;;### (autoloads (holes-insert-and-expand holes-abbrev-complete
@@ -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" (19107 64363))
+;;;;;;  "pg-pgip" "pg-pgip.el" (19108 51632))
 ;;; Generated autoloads from pg-pgip.el
 
-(autoload (quote pg-pgip-process-packet) "pg-pgip" "\
+(autoload '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 (quote pg-pgip-maybe-askpgip) "pg-pgip" "\
+(autoload 'pg-pgip-maybe-askpgip "pg-pgip" "\
 Send an <askpgip> message to the prover if PGIP is supported.
 
 \(fn)" nil nil)
 
-(autoload (quote pg-pgip-askprefs) "pg-pgip" "\
+(autoload 'pg-pgip-askprefs "pg-pgip" "\
 Send an <askprefs> message to the prover.
 
 \(fn)" nil nil)
@@ -301,63 +301,63 @@ All of these settings are optional.
 ;;;;;;  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" (19107 62480))
+;;;;;;  "pg-user" "pg-user.el" (19108 51656))
 ;;; Generated autoloads from pg-user.el
 
-(autoload (quote proof-define-assistant-command) "pg-user" "\
+(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.
 
 \(fn FN DOC CMDVAR &optional BODY)" nil (quote macro))
 
-(autoload (quote proof-define-assistant-command-witharg) "pg-user" "\
+(autoload 'proof-define-assistant-command-witharg "pg-user" "\
 Define command FN to prompt for string CMDVAR to proof assistant.
 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" "\
+(autoload 'proof-electric-terminator-enable "pg-user" "\
 Make sure the modeline is updated to display new value for electric terminator.
 
 \(fn)" nil nil)
 
-(autoload (quote pg-slow-fontify-tracing-hint) "pg-user" "\
+(autoload 'pg-slow-fontify-tracing-hint "pg-user" "\
 Not documented
 
 \(fn)" nil nil)
 
-(autoload (quote pg-response-buffers-hint) "pg-user" "\
+(autoload 'pg-response-buffers-hint "pg-user" "\
 Not documented
 
 \(fn &optional NEXTBUF)" nil nil)
 
-(autoload (quote pg-jump-to-end-hint) "pg-user" "\
+(autoload 'pg-jump-to-end-hint "pg-user" "\
 Not documented
 
 \(fn)" nil nil)
 
-(autoload (quote pg-processing-complete-hint) "pg-user" "\
+(autoload '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" "\
+(autoload 'pg-next-error-hint "pg-user" "\
 Display hint for locating error.
 
 \(fn)" nil nil)
 
-(autoload (quote pg-hint) "pg-user" "\
+(autoload '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" "\
+(autoload 'proof-imenu-enable "pg-user" "\
 Add or remove index menu.
 
 \(fn)" nil nil)
 
-(autoload (quote pg-previous-matching-input-from-input) "pg-user" "\
+(autoload 'pg-previous-matching-input-from-input "pg-user" "\
 Search backwards through input history for match for current input.
 \(Previous history elements are earlier commands.)
 With prefix argument N, search for Nth previous match.
@@ -365,7 +365,7 @@ If N is negative, search forwards for the -Nth following match.
 
 \(fn N)" t nil)
 
-(autoload (quote pg-next-matching-input-from-input) "pg-user" "\
+(autoload 'pg-next-matching-input-from-input "pg-user" "\
 Search forwards through input history for match for current input.
 \(Following history elements are more recent commands.)
 With prefix argument N, search for Nth following match.
@@ -373,32 +373,32 @@ If N is negative, search backwards for the -Nth previous match.
 
 \(fn N)" t nil)
 
-(autoload (quote pg-add-to-input-history) "pg-user" "\
+(autoload 'pg-add-to-input-history "pg-user" "\
 Maybe add CMD to the input history.
 CMD is only added to the input history if it is not a duplicate
 of the last item added.
 
 \(fn CMD)" nil nil)
 
-(autoload (quote pg-remove-from-input-history) "pg-user" "\
+(autoload 'pg-remove-from-input-history "pg-user" "\
 Maybe remove CMD from the end of the input history.
 This is called when the command is undone.  It's only
 removed if it matches the last item in the ring.
 
 \(fn CMD)" nil nil)
 
-(autoload (quote pg-clear-input-ring) "pg-user" "\
+(autoload 'pg-clear-input-ring "pg-user" "\
 Not documented
 
 \(fn)" nil nil)
 
 ;;;***
 
-;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (19107
-;;;;;;  55185))
+;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (19108
+;;;;;;  51674))
 ;;; Generated autoloads from pg-xml.el
 
-(autoload (quote pg-xml-parse-string) "pg-xml" "\
+(autoload 'pg-xml-parse-string "pg-xml" "\
 Parse string in ARG, same as pg-xml-parse-buffer.
 
 \(fn ARG)" nil nil)
@@ -406,7 +406,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" (19106 28181))
+;;;;;;  "proof-depends" "proof-depends.el" (19108 51693))
 ;;; Generated autoloads from proof-depends.el
 
 (autoload 'proof-depends-process-dependencies "proof-depends" "\
@@ -424,7 +424,7 @@ Make a portion of a context-sensitive menu showing proof dependencies.
 ;;;***
 
 ;;;### (autoloads (proof-easy-config) "proof-easy-config" "proof-easy-config.el"
-;;;;;;  (19106 28181))
+;;;;;;  (19108 4440))
 ;;; Generated autoloads from proof-easy-config.el
 
 (autoload 'proof-easy-config "proof-easy-config" "\
@@ -470,35 +470,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" (19107 64530))
+;;;;;;  "proof-menu" "proof-menu.el" (19108 51708))
 ;;; Generated autoloads from proof-menu.el
 
-(autoload (quote proof-menu-define-keys) "proof-menu" "\
+(autoload 'proof-menu-define-keys "proof-menu" "\
 Not documented
 
 \(fn MAP)" nil nil)
 
-(autoload (quote proof-menu-define-main) "proof-menu" "\
+(autoload 'proof-menu-define-main "proof-menu" "\
 Not documented
 
 \(fn)" nil nil)
 
-(autoload (quote proof-menu-define-specific) "proof-menu" "\
+(autoload 'proof-menu-define-specific "proof-menu" "\
 Not documented
 
 \(fn)" nil nil)
 
-(autoload (quote proof-aux-menu) "proof-menu" "\
+(autoload 'proof-aux-menu "proof-menu" "\
 Construct and return PG auxiliary menu used in non-scripting buffers.
 
 \(fn)" nil nil)
 
-(autoload (quote proof-defpacustom-fn) "proof-menu" "\
+(autoload 'proof-defpacustom-fn "proof-menu" "\
 As for macro `defpacustom' but evaluating arguments.
 
 \(fn NAME VAL ARGS)" nil nil)
 
-(autoload (quote defpacustom) "proof-menu" "\
+(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.
@@ -512,8 +512,11 @@ evaluate can be provided instead.
 
 ;;;***
 
+
+;;;***
+
 ;;;### (autoloads (proof-mmm-enable proof-mmm-set-global) "proof-mmm"
-;;;;;;  "proof-mmm.el" (19106 28181))
+;;;;;;  "proof-mmm.el" (19109 31675))
 ;;; Generated autoloads from proof-mmm.el
 
 (autoload 'proof-mmm-set-global "proof-mmm" "\
@@ -535,62 +538,62 @@ 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" (19107
-;;;;;;  65360))
+;;;;;;  proof-colour-locked) "proof-script" "proof-script.el" (19108
+;;;;;;  51751))
 ;;; Generated autoloads from proof-script.el
 
-(autoload (quote proof-colour-locked) "proof-script" "\
+(autoload 'proof-colour-locked "proof-script" "\
 Alter the colour of the locked region according to variable `proof-colour-locked'.
 
 \(fn)" t nil)
 
-(autoload (quote proof-unprocessed-begin) "proof-script" "\
+(autoload '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" "\
+(autoload '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" "\
+(autoload '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" "\
+(autoload '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" "\
+(autoload '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.
 
 \(fn SPAN &optional NOHIGHLIGHT)" nil nil)
 
-(autoload (quote proof-insert-pbp-command) "proof-script" "\
+(autoload 'proof-insert-pbp-command "proof-script" "\
 Insert CMD into the proof queue.
 
 \(fn CMD)" nil nil)
 
-(autoload (quote proof-insert-sendback-command) "proof-script" "\
+(autoload 'proof-insert-sendback-command "proof-script" "\
 Insert CMD into the proof script, execute assert-until-point.
 
 \(fn CMD)" nil nil)
 
-(autoload (quote proof-mode) "proof-script" "\
+(autoload 'proof-mode "proof-script" "\
 Proof General major mode class for proof scripts.
 \\{proof-mode-map}
 
 \(fn)" t nil)
 
-(autoload (quote proof-config-done) "proof-script" "\
+(autoload '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.
@@ -603,10 +606,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" (19107 65117))
+;;;;;;  "proof-shell.el" (19108 51779))
 ;;; Generated autoloads from proof-shell.el
 
-(autoload (quote proof-shell-ready-prover) "proof-shell" "\
+(autoload '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.
@@ -618,13 +621,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 (quote proof-shell-available-p) "proof-shell" "\
+(autoload '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 (quote proof-shell-insert) "proof-shell" "\
+(autoload '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
@@ -645,7 +648,7 @@ used in `proof-append-alist' when we start processing a queue, and in
 
 \(fn STRING ACTION &optional SCRIPTSPAN)" nil nil)
 
-(autoload (quote proof-start-queue) "proof-shell" "\
+(autoload '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.
@@ -654,7 +657,7 @@ This function calls `proof-append-alist'.
 
 \(fn START END ALIST)" nil nil)
 
-(autoload (quote proof-extend-queue) "proof-shell" "\
+(autoload '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.
@@ -662,7 +665,7 @@ The queue mode is set to 'advancing
 
 \(fn END ALIST)" nil nil)
 
-(autoload (quote proof-shell-wait) "proof-shell" "\
+(autoload '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
@@ -670,7 +673,7 @@ in some cases.   May be called by `proof-shell-invisible-command'.
 
 \(fn)" nil nil)
 
-(autoload (quote proof-shell-invisible-command) "proof-shell" "\
+(autoload '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.
@@ -692,7 +695,7 @@ If NOERROR is set, surpress usual error action.
 
 \(fn CMD &optional WAIT INVISIBLECALLBACK &rest FLAGS)" nil nil)
 
-(autoload (quote proof-shell-invisible-cmd-get-result) "proof-shell" "\
+(autoload '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
@@ -700,18 +703,18 @@ Ordinary output (and error handling) is disabled, and the result
 
 \(fn CMD)" nil nil)
 
-(autoload (quote proof-shell-invisible-command-invisible-result) "proof-shell" "\
+(autoload '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 (quote proof-shell-mode) "proof-shell" "\
+(autoload 'proof-shell-mode "proof-shell" "\
 Proof General shell mode class for proof assistant processes
 
 \(fn)" t nil)
 
-(autoload (quote proof-shell-config-done) "proof-shell" "\
+(autoload '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.
@@ -721,7 +724,7 @@ processing.
 ;;;***
 
 ;;;### (autoloads (proof-ready-for-assistant) "proof-site" "proof-site.el"
-;;;;;;  (19106 28181))
+;;;;;;  (19108 51789))
 ;;; Generated autoloads from proof-site.el
 
 (autoload 'proof-ready-for-assistant "proof-site" "\
@@ -733,7 +736,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" (19106 28181))
+;;;;;;  "proof-splash" "proof-splash.el" (19108 55485))
 ;;; Generated autoloads from proof-splash.el
 
 (autoload 'proof-splash-display-screen "proof-splash" "\
@@ -810,10 +813,10 @@ Turn on/off menu in all script buffers and ensure new buffers follow suit.
 ;;;***
 
 ;;;### (autoloads (scomint-make scomint-make-in-buffer) "scomint"
-;;;;;;  "../lib/scomint.el" (19107 62783))
+;;;;;;  "../lib/scomint.el" (19109 20818))
 ;;; Generated autoloads from ../lib/scomint.el
 
-(autoload (quote scomint-make-in-buffer) "scomint" "\
+(autoload 'scomint-make-in-buffer "scomint" "\
 Make a Comint process NAME in BUFFER, running PROGRAM.
 If BUFFER is nil, it defaults to NAME surrounded by `*'s.
 PROGRAM should be either a string denoting an executable program to create
@@ -826,7 +829,7 @@ If PROGRAM is a string, any more args are arguments to PROGRAM.
 
 \(fn NAME BUFFER PROGRAM &optional STARTFILE &rest SWITCHES)" nil nil)
 
-(autoload (quote scomint-make) "scomint" "\
+(autoload 'scomint-make "scomint" "\
 Make a Comint process NAME in a buffer, running PROGRAM.
 The name of the buffer is made by surrounding NAME with `*'s.
 PROGRAM should be either a string denoting an executable program to create
@@ -867,12 +870,22 @@ in your emacs font.
 
 ;;;***
 
+;;;### (autoloads (unicode-tokens-encode-str) "unicode-tokens" "../lib/unicode-tokens.el"
+;;;;;;  (19108 51332))
+;;; Generated autoloads from ../lib/unicode-tokens.el
+
+(autoload 'unicode-tokens-encode-str "unicode-tokens" "\
+Return a unicode encoded version presentation of STR.
+
+\(fn STR)" nil nil)
+
+;;;***
+
 ;;;### (autoloads nil nil ("../lib/local-vars-list.el" "../lib/pg-dev.el"
 ;;;;;;  "../lib/pg-fontsets.el" "../lib/proof-compat.el" "../lib/span.el"
-;;;;;;  "../lib/unicode-tokens.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")
-;;;;;;  (19107 65388 517192))
+;;;;;;  "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))
 
 ;;;***