Additions for maths menu

2 files changed, 279 insertions, 122 deletions

diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 907590ed..bd1b1862 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -2,46 +2,91 @@
 (if (featurep 'proof-autoloads) (error "Already loaded"))
 
 (provide 'proof-autoloads)
+
+
+;;;### (autoloads nil "bufhist" "../lib/bufhist.el" (17799 61158))
+;;; Generated autoloads from ../lib/bufhist.el
+
+(autoload (quote bufhist-mode) "bufhist" "\
+Minor mode retaining an in-memory history of the buffer contents.")
+
+;;;***
 
-;;;### (autoloads nil "_pkg" "generic/_pkg.el")
+;;;### (autoloads (holes-mode) "holes" "../lib/holes.el" (17641 26026))
+;;; Generated autoloads from ../lib/holes.el
 
-(package-provide 'ProofGeneral :version "3.3pre010320" :type 'regular)
+(autoload (quote holes-mode) "holes" "\
+If ARG is nil, then toggle holes mode on/off.
+If arg is positive, then turn holes mode on.  If arg is negative, then
+turn it off.
+
+\(fn &optional ARG)" t nil)
 
 ;;;***
 
-;;;### (autoloads (pg-pgip-askprefs pg-pgip-maybe-askpgip pg-pgip-process-packet) "pg-pgip" "generic/pg-pgip.el")
+;;;### (autoloads (maths-menu-mode) "maths-menu" "../lib/maths-menu.el"
+;;;;;;  (18271 52110))
+;;; Generated autoloads from ../lib/maths-menu.el
+
+(autoload (quote 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.
+This mode is only useful with a font which can display the maths repertoire.
 
-(autoload 'pg-pgip-process-packet "pg-pgip" "\
+\(fn &optional ARG)" t nil)
+
+;;;***
+
+;;;### (autoloads (pg-pgip-askprefs pg-pgip-maybe-askpgip pg-pgip-process-packet)
+;;;;;;  "pg-pgip" "pg-pgip.el" (18269 10080))
+;;; Generated autoloads from pg-pgip.el
+
+(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." nil nil)
+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" "\
-Send an <askpgip> message to the prover if PGIP is supported." nil nil)
+(autoload (quote pg-pgip-maybe-askpgip) "pg-pgip" "\
+Send an <askpgip> message to the prover if PGIP is supported.
 
-(autoload 'pg-pgip-askprefs "pg-pgip" "\
-Send an <askprefs> message to the prover." nil nil)
+\(fn)" nil nil)
+
+(autoload (quote pg-pgip-askprefs) "pg-pgip" "\
+Send an <askprefs> message to the prover.
+
+\(fn)" nil nil)
 
 ;;;***
 
-;;;### (autoloads (pg-response-has-error-location proof-next-error) "pg-response" "generic/pg-response.el")
+;;;### (autoloads (pg-response-has-error-location proof-next-error)
+;;;;;;  "pg-response" "pg-response.el" (18269 10080))
+;;; Generated autoloads from pg-response.el
 
-(autoload 'proof-next-error "pg-response" "\
+(autoload (quote proof-next-error) "pg-response" "\
 Jump to location of next error reported in the response buffer.
 
 A prefix arg specifies how many error messages to move;
 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)
+and start at the first error.
 
-(autoload 'pg-response-has-error-location "pg-response" "\
+\(fn &optional ARGP)" t nil)
+
+(autoload (quote 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)
+See `pg-next-error-regexp'.
+
+\(fn)" nil nil)
 
 ;;;***
 
-;;;### (autoloads (pg-defthymode) "pg-thymodes" "generic/pg-thymodes.el")
+;;;### (autoloads (pg-defthymode) "pg-thymodes" "pg-thymodes.el"
+;;;;;;  (16513 49231))
+;;; Generated autoloads from pg-thymodes.el
 
-(autoload 'pg-defthymode "pg-thymodes" "\
+(autoload (quote 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:
@@ -52,80 +97,147 @@ can define a number of variables for the mode, viz:
   SYM-<parent-mode>		(defaults to fundamental-mode)
   SYM-<filename-regexp>	        (regexp matching filenames for auto-mode-alist)
 
-All of these settings are optional." nil 'macro)
+All of these settings are optional.
+
+\(fn SYM NAME &rest BODY)" nil (quote macro))
 
 ;;;***
 
-;;;### (autoloads (proof-define-assistant-command-witharg proof-define-assistant-command) "pg-user" "generic/pg-user.el")
+;;;### (autoloads (proof-define-assistant-command-witharg proof-define-assistant-command)
+;;;;;;  "pg-user" "pg-user.el" (18271 11570))
+;;; Generated autoloads from pg-user.el
 
-(autoload 'proof-define-assistant-command "pg-user" "\
+(autoload (quote proof-define-assistant-command) "pg-user" "\
 Define command FN to send string BODY to proof assistant, based on CMDVAR.
-BODY defaults to CMDVAR, a variable." nil 'macro)
+BODY defaults to CMDVAR, a variable.
+
+\(fn FN DOC CMDVAR &optional BODY)" nil (quote macro))
 
-(autoload 'proof-define-assistant-command-witharg "pg-user" "\
+(autoload (quote 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." nil 'macro)
+CMDVAR is a variable holding a function or string.  Automatically has history.
+
+\(fn FN DOC CMDVAR PROMPT &rest BODY)" nil (quote macro))
 
 ;;;***
 
-;;;### (autoloads (pg-xml-parse-string) "pg-xml" "generic/pg-xml.el")
+;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (18268
+;;;;;;  11587))
+;;; Generated autoloads from pg-xml.el
 
-(autoload 'pg-xml-parse-string "pg-xml" "\
-Parse string in ARG, same as pg-xml-parse-buffer." nil nil)
+(autoload (quote pg-xml-parse-string) "pg-xml" "\
+Parse string in ARG, same as pg-xml-parse-buffer.
+
+\(fn ARG)" nil nil)
 
 ;;;***
 
-;;;### (autoloads (proof-dependency-in-span-context-menu proof-depends-process-dependencies) "proof-depends" "generic/proof-depends.el")
+;;;### (autoloads (proof-dependency-in-span-context-menu proof-depends-process-dependencies)
+;;;;;;  "proof-depends" "proof-depends.el" (16513 49231))
+;;; Generated autoloads from proof-depends.el
 
-(autoload 'proof-depends-process-dependencies "proof-depends" "\
+(autoload (quote proof-depends-process-dependencies) "proof-depends" "\
 Process dependencies reported by prover, for NAME in span GSPAN.
 Called from `proof-done-advancing' when a save is processed and
-proof-last-theorem-dependencies is set." nil nil)
+proof-last-theorem-dependencies is set.
+
+\(fn NAME GSPAN)" nil nil)
 
-(autoload 'proof-dependency-in-span-context-menu "proof-depends" "\
-Make a portion of a context-sensitive menu showing proof dependencies." nil nil)
+(autoload (quote proof-dependency-in-span-context-menu) "proof-depends" "\
+Make a portion of a context-sensitive menu showing proof dependencies.
+
+\(fn SPAN)" nil nil)
 
 ;;;***
 
-;;;### (autoloads (proof-easy-config) "proof-easy-config" "generic/proof-easy-config.el")
+;;;### (autoloads (proof-easy-config) "proof-easy-config" "proof-easy-config.el"
+;;;;;;  (16513 49231))
+;;; Generated autoloads from proof-easy-config.el
+
+(autoload (quote proof-easy-config) "proof-easy-config" "\
+Configure Proof General for proof-assistant using BODY as a setq body.
+The symbol SYM and string name NAME must match those given in
+the `proof-assistant-table', which see.
 
-(autoload 'proof-easy-config "proof-easy-config" "\
-Configure Proof General for proof-assistant using BODY as a setq body." nil 'macro)
+\(fn SYM NAME &rest BODY)" nil (quote macro))
 
 ;;;***
 
-;;;### (autoloads (proof-indent-line) "proof-indent" "generic/proof-indent.el")
+;;;### (autoloads (proof-indent-line) "proof-indent" "proof-indent.el"
+;;;;;;  (17893 29685))
+;;; Generated autoloads from proof-indent.el
+
+(autoload (quote proof-indent-line) "proof-indent" "\
+Indent current line of proof script, if indentation enabled.
 
-(autoload 'proof-indent-line "proof-indent" "\
-Indent current line of proof script, if indentation enabled." t nil)
+\(fn)" t nil)
 
 ;;;***
 
-;;;### (autoloads (defpacustom proof-defpacustom-fn proof-definvisible proof-defshortcut proof-menu-define-specific proof-menu-define-main proof-menu-define-keys) "proof-menu" "generic/proof-menu.el")
+;;;### (autoloads (proof-maths-menu-enable proof-maths-menu-support-available)
+;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (18271 52951))
+;;; Generated autoloads from proof-maths-menu.el
+
+(autoload (quote proof-maths-menu-support-available) "proof-maths-menu" "\
+A test to see whether maths-menu support is available.
+
+\(fn)" nil nil)
+
+(autoload (quote proof-maths-menu-enable) "proof-maths-menu" "\
+Turn on or off maths-menu mode in Proof General script buffer.
+This invokes `maths-menu-mode' to toggle the setting for the current
+buffer, and then sets PG's option for default to match.
+Also we arrange to have maths menu mode turn itself on automatically 
+in future if we have just activated it for this buffer.
+
+\(fn)" t nil)
+
+;;;***
+
+;;;### (autoloads (defpacustom proof-defpacustom-fn proof-definvisible
+;;;;;;  proof-defshortcut proof-menu-define-specific proof-menu-define-main
+;;;;;;  proof-menu-define-keys) "proof-menu" "proof-menu.el" (18271
+;;;;;;  52994))
+;;; Generated autoloads from proof-menu.el
+
+(autoload (quote proof-menu-define-keys) "proof-menu" "\
+Not documented
+
+\(fn MAP)" nil nil)
+
+(autoload (quote proof-menu-define-main) "proof-menu" "\
+Not documented
 
-(autoload 'proof-menu-define-keys "proof-menu" nil nil nil)
+\(fn)" nil nil)
 
-(autoload 'proof-menu-define-main "proof-menu" nil nil nil)
+(autoload (quote proof-menu-define-specific) "proof-menu" "\
+Not documented
 
-(autoload 'proof-menu-define-specific "proof-menu" nil nil nil)
+\(fn)" nil nil)
 
-(autoload 'proof-defshortcut "proof-menu" "\
+(autoload (quote proof-defshortcut) "proof-menu" "\
 Define shortcut function FN to insert STRING, optional keydef KEY.
 This is intended for defining proof assistant specific functions.
 STRING is inserted using `proof-insert', which see.
-KEY is added onto proof-assistant map." nil 'macro)
+KEY is added onto proof-assistant map.
 
-(autoload 'proof-definvisible "proof-menu" "\
+\(fn FN STRING &optional KEY)" nil (quote macro))
+
+(autoload (quote proof-definvisible) "proof-menu" "\
 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)
+KEY is added onto proof-assistant map.
+
+\(fn FN STRING &optional KEY)" nil (quote macro))
+
+(autoload (quote proof-defpacustom-fn) "proof-menu" "\
+As for macro `defpacustom' but evaluating arguments.
 
-(autoload 'proof-defpacustom-fn "proof-menu" "\
-As for macro `defpacustom' but evaluating arguments." nil nil)
+\(fn NAME VAL ARGS)" nil nil)
 
-(autoload 'defpacustom "proof-menu" "\
+(autoload (quote 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.
@@ -133,62 +245,84 @@ 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." nil 'macro)
+evaluate can be provided instead.
+
+\(fn NAME VAL &rest ARGS)" nil (quote macro))
 
 ;;;***
 
-;;;### (autoloads (proof-mmm-enable proof-mmm-support-available) "proof-mmm" "generic/proof-mmm.el")
+;;;### (autoloads (proof-mmm-enable proof-mmm-support-available)
+;;;;;;  "proof-mmm" "proof-mmm.el" (18268 11505))
+;;; Generated autoloads from proof-mmm.el
+
+(autoload (quote proof-mmm-support-available) "proof-mmm" "\
+A test to see whether mmm support is available.
 
-(autoload 'proof-mmm-support-available "proof-mmm" "\
-A test to see whether mmm support is available." nil nil)
+\(fn)" nil nil)
 
-(autoload 'proof-mmm-enable "proof-mmm" "\
-Turn on or off MMM mode in Proof General script buffers.
+(autoload (quote proof-mmm-enable) "proof-mmm" "\
+Turn on or off MMM mode in Proof General script buffer.
 This invokes `mmm-mode' to toggle the setting for the current
-buffer, and then sets PG's option for the setting accordingly." nil nil)
+buffer, and then sets PG's option for default to match.
+Also we arrange to have MMM mode turn itself on automatically 
+in future if we have just activated it for this buffer.
 
-;;;***
-
-;;;### (autoloads nil "proof-script" "generic/proof-script.el")
+\(fn)" t nil)
 
 ;;;***
 
-;;;### (autoloads (proof-shell-invisible-command proof-shell-wait proof-extend-queue proof-start-queue proof-shell-available-p proof-shell-live-buffer proof-shell-ready-prover) "proof-shell" "generic/proof-shell.el")
+;;;### (autoloads (proof-shell-invisible-command proof-shell-wait
+;;;;;;  proof-extend-queue proof-start-queue proof-shell-available-p
+;;;;;;  proof-shell-live-buffer proof-shell-ready-prover) "proof-shell"
+;;;;;;  "proof-shell.el" (18120 5775))
+;;; 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.
 Otherwise, if the shell is busy, give an error.
-No change to current buffer or point." nil nil)
+No change to current buffer or point.
+
+\(fn &optional QUEUEMODE)" nil nil)
+
+(autoload (quote proof-shell-live-buffer) "proof-shell" "\
+Return buffer of active proof assistant, or nil if none running.
 
-(autoload 'proof-shell-live-buffer "proof-shell" "\
-Return buffer of active proof assistant, or nil if none running." nil nil)
+\(fn)" nil nil)
 
-(autoload 'proof-shell-available-p "proof-shell" "\
+(autoload (quote proof-shell-available-p) "proof-shell" "\
 Returns non-nil if there is a proof shell active and available.
-No error messages.  Useful as menu or toolbar enabler." nil nil)
+No error messages.  Useful as menu or toolbar enabler.
 
-(autoload 'proof-start-queue "proof-shell" "\
+\(fn)" nil nil)
+
+(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.
 
-This function calls `proof-append-alist'." nil nil)
+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.
-The queue mode is set to 'advancing" nil nil)
+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
-in some cases.   May be called by `proof-shell-invisible-command'." nil nil)
+in some cases.   May be called by `proof-shell-invisible-command'.
 
-(autoload 'proof-shell-invisible-command "proof-shell" "\
+\(fn)" nil nil)
+
+(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.
@@ -200,103 +334,118 @@ 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.
 
-In case CMD is (or yields) nil, do nothing." nil nil)
+In case CMD is (or yields) nil, do nothing.
+
+\(fn CMD &optional WAIT)" nil nil)
 
 ;;;***
 
-;;;### (autoloads (proof-splash-message proof-splash-display-screen) "proof-splash" "generic/proof-splash.el")
+;;;### (autoloads (proof-splash-message proof-splash-display-screen)
+;;;;;;  "proof-splash" "proof-splash.el" (18271 10299))
+;;; Generated autoloads from proof-splash.el
 
-(autoload 'proof-splash-display-screen "proof-splash" "\
+(autoload (quote proof-splash-display-screen) "proof-splash" "\
 Save window config and display Proof General splash screen.
 If TIMEOUT is non-nil, time out outside this function, definitely
 by end of configuring proof mode.
-Otherwise, timeout inside this function after 10 seconds or so." t nil)
+Otherwise, timeout inside this function after 10 seconds or so.
 
-(autoload 'proof-splash-message "proof-splash" "\
-Make sure the user gets welcomed one way or another." t nil)
+\(fn &optional TIMEOUT)" t nil)
+
+(autoload (quote proof-splash-message) "proof-splash" "\
+Make sure the user gets welcomed one way or another.
+
+\(fn)" t nil)
 
 ;;;***
 
-;;;### (autoloads (proof-format) "proof-syntax" "generic/proof-syntax.el")
+;;;### (autoloads (proof-format) "proof-syntax" "proof-syntax.el"
+;;;;;;  (17987 35833))
+;;; Generated autoloads from proof-syntax.el
 
-(autoload 'proof-format "proof-syntax" "\
+(autoload (quote proof-format) "proof-syntax" "\
 Format a string by matching regexps in ALIST against STRING.
 ALIST contains (REGEXP . REPLACEMENT) pairs where REPLACEMENT
-may be a string or sexp evaluated to get a string." nil nil)
+may be a string or sexp evaluated to get a string.
+
+\(fn ALIST STRING)" nil nil)
 
 ;;;***
 
-;;;### (autoloads (proof-toolbar-setup) "proof-toolbar" "generic/proof-toolbar.el")
+;;;### (autoloads (proof-toolbar-setup) "proof-toolbar" "proof-toolbar.el"
+;;;;;;  (18271 10299))
+;;; Generated autoloads from proof-toolbar.el
 
-(autoload 'proof-toolbar-setup "proof-toolbar" "\
+(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." t nil)
+to the default toolbar.
+
+\(fn)" t nil)
 
 ;;;***
 
-;;;### (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")
+;;;### (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" "proof-x-symbol.el" (18269 9038))
+;;; Generated autoloads from 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 (quote proof-x-symbol-support-maybe-available) "proof-x-symbol" "\
+A test to see whether x-symbol support may be available.
 
-(autoload 'proof-x-symbol-enable "proof-x-symbol" "\
+\(fn)" nil nil)
+
+(autoload (quote proof-x-symbol-enable) "proof-x-symbol" "\
 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)
+in future if we have just activated it for this buffer.
 
-(defalias 'proof-x-symbol-decode-region 'x-symbol-decode-region)
+\(fn)" nil nil)
 
-(autoload 'proof-x-symbol-shell-config "proof-x-symbol" "\
-Configure the proof shell for x-symbol, if proof-x-symbol-support<>nil.
-Assumes that the current buffer is the proof shell buffer." nil nil)
+(defalias (quote proof-x-symbol-decode-region) (quote x-symbol-decode-region))
 
-(autoload 'proof-x-symbol-config-output-buffer "proof-x-symbol" "\
-Configure the current output buffer (goals/response/trace) for X-Symbol." nil nil)
+(autoload (quote proof-x-symbol-shell-config) "proof-x-symbol" "\
+Configure the proof shell for x-symbol, if proof-x-symbol-support<>nil.
+Assumes that the current buffer is the proof shell buffer.
 
-;;;***
-
-;;;### (autoloads (bufhist-checkpoint) "bufhist" "lib/bufhist.el")
+\(fn)" nil nil)
 
-(autoload 'bufhist-checkpoint "bufhist" "\
-Add the current buffer contents to the ring history." t nil)
+(autoload (quote proof-x-symbol-config-output-buffer) "proof-x-symbol" "\
+Configure the current output buffer (goals/response/trace) for X-Symbol.
 
-(autoload 'bufhist-mode "bufhist" "\
-Minor mode retaining an in-memory history of the buffer contents.")
+\(fn)" nil nil)
 
 ;;;***
 
-;;;### (autoloads nil "bufregring" "lib/bufregring.el")
-
-(autoload 'bufhist-mode "bufhist" "\
-Minor mode retaining an in-memory history of the buffer contents.")
+;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "../lib/texi-docstring-magic.el"
+;;;;;;  (18269 10371))
+;;; Generated autoloads from ../lib/texi-docstring-magic.el
 
-;;;***
-
-;;;### (autoloads nil "bufregs" "lib/bufregs.el")
+(autoload (quote 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).
 
-(autoload 'bufregs-mode "bufregs" "\
-Minor mode retaining an in-memory history of the buffer contents.")
+\(fn &optional NOERROR)" t nil)
 
 ;;;***
 
-;;;### (autoloads (holes-mode) "holes" "lib/holes.el")
-
-(autoload 'holes-mode "holes" "\
-If ARG is nil, then toggle holes mode on/off.
-If arg is positive, then turn holes mode on.  If arg is negative, then
-turn it off." t nil)
+;;;### (autoloads nil nil ("../lib/holes-load.el" "../lib/local-vars-list.el"
+;;;;;;  "../lib/proof-compat.el" "../lib/span-extent.el" "../lib/span-overlay.el"
+;;;;;;  "../lib/span.el" "../lib/unichars.el" "../lib/xml-fixed.el"
+;;;;;;  "../lib/xmlunicode.el" "pg-assoc.el" "pg-autotest.el" "pg-festival.el"
+;;;;;;  "pg-goals.el" "pg-metadata.el" "pg-pbrpm.el" "pg-pgip-old.el"
+;;;;;;  "pg-xhtml.el" "proof-config.el" "proof-script.el" "proof-site.el"
+;;;;;;  "proof-system.el" "proof-utils.el" "proof.el") (18271 52998
+;;;;;;  138163))
 
 ;;;***
 
-;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "lib/texi-docstring-magic.el")
+;;;### (autoloads nil "_pkg" "_pkg.el" (16513 49231))
+;;; Generated autoloads from _pkg.el
 
-(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)." t nil)
+(package-provide (quote ProofGeneral) :version "3.3pre010320" :type (quote regular))
 
 ;;;***
-
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 2333541f..9591b914 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -268,6 +268,7 @@ without adjusting window layout."
 
 (proof-deftoggle-fn 'proof-imenu-enable 'proof-imenu-toggle)
 (proof-deftoggle-fn (proof-ass-sym x-symbol-enable) 'proof-x-symbol-toggle)
+(proof-deftoggle-fn (proof-ass-sym maths-menu-enable) 'proof-maths-menu-toggle)
 (proof-deftoggle-fn (proof-ass-sym mmm-enable) 'proof-mmm-toggle)
 
 ;; TODO (low priority): add dynamic enable-disable
@@ -304,6 +305,12 @@ without adjusting window layout."
       :active (proof-x-symbol-support-maybe-available)
       :style toggle
       :selected (and (boundp 'x-symbol-mode) x-symbol-mode)]
+
+     ["Maths Menu" (proof-maths-menu-toggle (if maths-menu-mode 0 1))
+      :active (proof-maths-menu-support-available)
+      :style toggle
+      :selected (and (boundp 'maths-menu-mode) maths-menu-mode)]
+ 
      ["Multiple Modes" (proof-mmm-toggle (if mmm-mode 0 1))
       :active (proof-mmm-support-available)
       :style toggle
@@ -397,6 +404,7 @@ without adjusting window layout."
    ;;'proof-output-fontify-enable
    'proof-strict-read-only
    (proof-ass-sym x-symbol-enable)
+   (proof-ass-sym maths-menu-enable)
    (proof-ass-sym mmm-enable)
    'proof-toolbar-enable
    'proof-keep-response-history