diff options
Diffstat (limited to 'generic/proof-autoloads.el')
| -rw-r--r-- | generic/proof-autoloads.el | 260 |
1 files changed, 146 insertions, 114 deletions
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el index 703258ff..798fb440 100644 --- a/generic/proof-autoloads.el +++ b/generic/proof-autoloads.el @@ -8,7 +8,7 @@ ;;;*** ;;;### (autoloads (bufhist-exit bufhist-init bufhist-mode) "bufhist" -;;;;;; "../lib/bufhist.el" (19108 53141)) +;;;;;; "../lib/bufhist.el" (19110 10300)) ;;; Generated autoloads from ../lib/bufhist.el (autoload 'bufhist-mode "bufhist" "\ @@ -41,15 +41,15 @@ Stop keeping ring history for current buffer. ;;;### (autoloads (holes-insert-and-expand holes-abbrev-complete ;;;;;; holes-mode holes-set-make-active-hole) "holes" "../lib/holes.el" -;;;;;; (19107 61958)) +;;;;;; (19110 10300)) ;;; Generated autoloads from ../lib/holes.el -(autoload (quote holes-set-make-active-hole) "holes" "\ +(autoload 'holes-set-make-active-hole "holes" "\ Make a new hole between START and END or at point, and make it active. \(fn &optional START END)" t nil) -(autoload (quote holes-mode) "holes" "\ +(autoload 'holes-mode "holes" "\ Toggle Holes minor mode. With arg, turn Outline minor mode on if arg is positive, off otherwise. @@ -139,7 +139,7 @@ undoing on holes cannot make holes re-appear. \(fn &optional ARG)" t nil) -(autoload (quote holes-abbrev-complete) "holes" "\ +(autoload 'holes-abbrev-complete "holes" "\ Complete abbrev by putting holes and indenting. Moves point at beginning of expanded text. Put this function as call-back for your abbrevs, and just expanded \"#\" and \"@{..}\" will @@ -147,7 +147,7 @@ become holes. \(fn)" nil nil) -(autoload (quote holes-insert-and-expand) "holes" "\ +(autoload 'holes-insert-and-expand "holes" "\ Insert S, expand it and replace #s and @{]s by holes. \(fn S)" nil nil) @@ -155,10 +155,10 @@ Insert S, expand it and replace #s and @{]s by holes. ;;;*** ;;;### (autoloads (maths-menu-mode) "maths-menu" "../lib/maths-menu.el" -;;;;;; (19107 62723)) +;;;;;; (19110 10300)) ;;; Generated autoloads from ../lib/maths-menu.el -(autoload (quote maths-menu-mode) "maths-menu" "\ +(autoload '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. @@ -169,16 +169,16 @@ This mode is only useful with a font which can display the maths repertoire. ;;;*** ;;;### (autoloads (proof-associated-windows proof-associated-buffers) -;;;;;; "pg-assoc" "pg-assoc.el" (19107 62126)) +;;;;;; "pg-assoc" "pg-assoc.el" (19110 10300)) ;;; Generated autoloads from pg-assoc.el -(autoload (quote proof-associated-buffers) "pg-assoc" "\ +(autoload 'proof-associated-buffers "pg-assoc" "\ Return a list of the associated buffers. Some may be dead/nil. \(fn)" nil nil) -(autoload (quote proof-associated-windows) "pg-assoc" "\ +(autoload 'proof-associated-windows "pg-assoc" "\ Return a list of the associated buffers windows. Dead or nil buffers are not represented in the list. @@ -187,10 +187,10 @@ Dead or nil buffers are not represented in the list. ;;;*** ;;;### (autoloads (proof-goals-config-done) "pg-goals" "pg-goals.el" -;;;;;; (19107 49109)) +;;;;;; (19110 10300)) ;;; Generated autoloads from pg-goals.el -(autoload (quote proof-goals-config-done) "pg-goals" "\ +(autoload 'proof-goals-config-done "pg-goals" "\ Initialise the goals buffer after the child has been configured. \(fn)" nil nil) @@ -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" (19108 51632)) +;;;;;; "pg-pgip" "pg-pgip.el" (19110 13559)) ;;; Generated autoloads from pg-pgip.el -(autoload 'pg-pgip-process-packet "pg-pgip" "\ +(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. \(fn PGIPS)" nil nil) -(autoload 'pg-pgip-maybe-askpgip "pg-pgip" "\ +(autoload (quote pg-pgip-maybe-askpgip) "pg-pgip" "\ Send an <askpgip> message to the prover if PGIP is supported. \(fn)" nil nil) -(autoload 'pg-pgip-askprefs "pg-pgip" "\ +(autoload (quote pg-pgip-askprefs) "pg-pgip" "\ Send an <askprefs> message to the prover. \(fn)" nil nil) @@ -220,9 +220,9 @@ Send an <askprefs> message to the prover. ;;;*** ;;;### (autoloads (pg-response-has-error-location proof-next-error -;;;;;; pg-response-display-with-face pg-response-maybe-erase proof-response-config-done -;;;;;; proof-response-mode) "pg-response" "pg-response.el" (19107 -;;;;;; 62473)) +;;;;;; pg-response-message pg-response-display-with-face pg-response-maybe-erase +;;;;;; proof-response-config-done proof-response-mode) "pg-response" +;;;;;; "pg-response.el" (19112 23312)) ;;; Generated autoloads from pg-response.el (autoload (quote proof-response-mode) "pg-response" "\ @@ -251,10 +251,14 @@ Returns non-nil if response buffer was cleared. (autoload (quote pg-response-display-with-face) "pg-response" "\ Display STR with FACE in response buffer. -Also updates `proof-shell-last-output'. \(fn STR &optional FACE)" nil nil) +(autoload (quote pg-response-message) "pg-response" "\ +Issue the message ARGS in the response buffer and display it. + +\(fn &rest ARGS)" nil nil) + (autoload (quote proof-next-error) "pg-response" "\ Jump to location of next error reported in the response buffer. @@ -275,10 +279,10 @@ See `pg-next-error-regexp'. ;;;*** ;;;### (autoloads (pg-defthymode) "pg-thymodes" "pg-thymodes.el" -;;;;;; (19107 62476)) +;;;;;; (19110 10300)) ;;; Generated autoloads from pg-thymodes.el -(autoload (quote pg-defthymode) "pg-thymodes" "\ +(autoload '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: @@ -300,10 +304,24 @@ All of these settings are optional. ;;;;;; pg-previous-matching-input-from-input proof-imenu-enable ;;;;;; 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" (19108 51656)) +;;;;;; proof-define-assistant-command-witharg proof-define-assistant-command +;;;;;; proof-goto-point proof-script-new-command-advance) "pg-user" +;;;;;; "pg-user.el" (19110 10300)) ;;; Generated autoloads from pg-user.el +(autoload 'proof-script-new-command-advance "pg-user" "\ +Move point to a nice position for a new command. +Assumes that point is at the end of a command. + +\(fn)" t nil) + +(autoload 'proof-goto-point "pg-user" "\ +Assert or retract to the command at current position. +Calls `proof-assert-until-point' or `proof-retract-until-point' as +appropriate. + +\(fn)" t nil) + (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. @@ -394,8 +412,8 @@ Not documented ;;;*** -;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (19108 -;;;;;; 51674)) +;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (19110 +;;;;;; 10300)) ;;; Generated autoloads from pg-xml.el (autoload 'pg-xml-parse-string "pg-xml" "\ @@ -406,7 +424,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" (19108 51693)) +;;;;;; "proof-depends" "proof-depends.el" (19110 10300)) ;;; Generated autoloads from proof-depends.el (autoload 'proof-depends-process-dependencies "proof-depends" "\ @@ -424,7 +442,7 @@ Make a portion of a context-sensitive menu showing proof dependencies. ;;;*** ;;;### (autoloads (proof-easy-config) "proof-easy-config" "proof-easy-config.el" -;;;;;; (19108 4440)) +;;;;;; (19110 10300)) ;;; Generated autoloads from proof-easy-config.el (autoload 'proof-easy-config "proof-easy-config" "\ @@ -437,7 +455,7 @@ the `proof-assistant-table', which see. ;;;*** ;;;### (autoloads (proof-indent-line) "proof-indent" "proof-indent.el" -;;;;;; (19106 28181)) +;;;;;; (19110 10300)) ;;; Generated autoloads from proof-indent.el (autoload 'proof-indent-line "proof-indent" "\ @@ -448,7 +466,7 @@ Indent current line of proof script, if indentation enabled. ;;;*** ;;;### (autoloads (proof-maths-menu-enable proof-maths-menu-set-global) -;;;;;; "proof-maths-menu" "proof-maths-menu.el" (19106 28181)) +;;;;;; "proof-maths-menu" "proof-maths-menu.el" (19110 10300)) ;;; Generated autoloads from proof-maths-menu.el (autoload 'proof-maths-menu-set-global "proof-maths-menu" "\ @@ -468,55 +486,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" (19108 51708)) +;;;### (autoloads (proof-aux-menu proof-menu-define-specific proof-menu-define-main +;;;;;; proof-menu-define-keys) "proof-menu" "proof-menu.el" (19112 +;;;;;; 23313)) ;;; Generated autoloads from proof-menu.el -(autoload 'proof-menu-define-keys "proof-menu" "\ -Not documented +(autoload (quote proof-menu-define-keys) "proof-menu" "\ +Prover specific keymap under C-c C-a. \(fn MAP)" nil nil) -(autoload 'proof-menu-define-main "proof-menu" "\ +(autoload (quote proof-menu-define-main) "proof-menu" "\ Not documented \(fn)" nil nil) -(autoload 'proof-menu-define-specific "proof-menu" "\ +(autoload (quote proof-menu-define-specific) "proof-menu" "\ Not documented \(fn)" nil nil) -(autoload 'proof-aux-menu "proof-menu" "\ +(autoload (quote proof-aux-menu) "proof-menu" "\ Construct and return PG auxiliary menu used in non-scripting buffers. \(fn)" nil nil) -(autoload 'proof-defpacustom-fn "proof-menu" "\ -As for macro `defpacustom' but evaluating arguments. - -\(fn NAME VAL ARGS)" nil nil) - -(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. -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. - -\(fn NAME VAL &rest ARGS)" nil (quote macro)) - -;;;*** - - ;;;*** ;;;### (autoloads (proof-mmm-enable proof-mmm-set-global) "proof-mmm" -;;;;;; "proof-mmm.el" (19109 31675)) +;;;;;; "proof-mmm.el" (19110 10300)) ;;; Generated autoloads from proof-mmm.el (autoload 'proof-mmm-set-global "proof-mmm" "\ @@ -536,64 +534,81 @@ 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" (19108 -;;;;;; 51751)) +;;;;;; proof-insert-pbp-command proof-register-possibly-new-processed-file +;;;;;; 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" (19112 23313)) ;;; Generated autoloads from proof-script.el -(autoload 'proof-colour-locked "proof-script" "\ +(autoload (quote proof-colour-locked) "proof-script" "\ Alter the colour of the locked region according to variable `proof-colour-locked'. \(fn)" t nil) -(autoload 'proof-unprocessed-begin "proof-script" "\ +(autoload (quote 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 'proof-locked-end "proof-script" "\ +(autoload (quote 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 'proof-locked-region-full-p "proof-script" "\ +(autoload (quote 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 'proof-locked-region-empty-p "proof-script" "\ +(autoload (quote proof-locked-region-empty-p) "proof-script" "\ Non-nil if the locked region is empty. Works on any buffer. \(fn)" nil nil) -(autoload 'pg-set-span-helphighlights "proof-script" "\ +(autoload (quote 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. +Argumen FACE means add face property FACE. -\(fn SPAN &optional NOHIGHLIGHT)" nil nil) +\(fn SPAN &optional NOHIGHLIGHT FACE)" nil nil) -(autoload 'proof-insert-pbp-command "proof-script" "\ +(autoload (quote proof-register-possibly-new-processed-file) "proof-script" "\ +Register a possibly new FILE as having been processed by the prover. + +If INFORMPROVER is non-nil, the proof assistant will be told about this, +to co-ordinate with its internal file-management. (Otherwise we assume +that it is a message from the proof assistant which triggers this call). +In this case, the user will be queried to save some buffers, unless +NOQUESTIONS is non-nil. + +No action is taken if the file is already registered. + +A warning message is issued if the register request came from the +proof assistant and Emacs has a modified buffer visiting the file. + +\(fn FILE &optional INFORMPROVER NOQUESTIONS)" nil nil) + +(autoload (quote proof-insert-pbp-command) "proof-script" "\ Insert CMD into the proof queue. \(fn CMD)" nil nil) -(autoload 'proof-insert-sendback-command "proof-script" "\ +(autoload (quote proof-insert-sendback-command) "proof-script" "\ Insert CMD into the proof script, execute assert-until-point. \(fn CMD)" nil nil) -(autoload 'proof-mode "proof-script" "\ +(autoload (quote proof-mode) "proof-script" "\ Proof General major mode class for proof scripts. \\{proof-mode-map} \(fn)" t nil) -(autoload 'proof-config-done "proof-script" "\ +(autoload (quote 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. @@ -606,10 +621,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" (19108 51779)) +;;;;;; "proof-shell.el" (19112 23489)) ;;; 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. @@ -621,13 +636,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 'proof-shell-available-p "proof-shell" "\ +(autoload (quote 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 'proof-shell-insert "proof-shell" "\ +(autoload (quote 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 @@ -648,7 +663,7 @@ used in `proof-append-alist' when we start processing a queue, and in \(fn STRING ACTION &optional SCRIPTSPAN)" nil nil) -(autoload 'proof-start-queue "proof-shell" "\ +(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. @@ -657,7 +672,7 @@ 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. @@ -665,7 +680,7 @@ 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 @@ -673,7 +688,7 @@ in some cases. May be called by `proof-shell-invisible-command'. \(fn)" nil nil) -(autoload 'proof-shell-invisible-command "proof-shell" "\ +(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. @@ -695,7 +710,7 @@ If NOERROR is set, surpress usual error action. \(fn CMD &optional WAIT INVISIBLECALLBACK &rest FLAGS)" nil nil) -(autoload 'proof-shell-invisible-cmd-get-result "proof-shell" "\ +(autoload (quote 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 @@ -703,18 +718,18 @@ Ordinary output (and error handling) is disabled, and the result \(fn CMD)" nil nil) -(autoload 'proof-shell-invisible-command-invisible-result "proof-shell" "\ +(autoload (quote 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 'proof-shell-mode "proof-shell" "\ +(autoload (quote proof-shell-mode) "proof-shell" "\ Proof General shell mode class for proof assistant processes \(fn)" t nil) -(autoload 'proof-shell-config-done "proof-shell" "\ +(autoload (quote 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. @@ -724,7 +739,7 @@ processing. ;;;*** ;;;### (autoloads (proof-ready-for-assistant) "proof-site" "proof-site.el" -;;;;;; (19108 51789)) +;;;;;; (19110 10300)) ;;; Generated autoloads from proof-site.el (autoload 'proof-ready-for-assistant "proof-site" "\ @@ -736,7 +751,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" (19108 55485)) +;;;;;; "proof-splash" "proof-splash.el" (19110 10300)) ;;; Generated autoloads from proof-splash.el (autoload 'proof-splash-display-screen "proof-splash" "\ @@ -753,7 +768,7 @@ Make sure the user gets welcomed one way or another. ;;;*** ;;;### (autoloads (proof-splice-separator proof-format) "proof-syntax" -;;;;;; "proof-syntax.el" (19107 64438)) +;;;;;; "proof-syntax.el" (19112 23313)) ;;; Generated autoloads from proof-syntax.el (autoload (quote proof-format) "proof-syntax" "\ @@ -771,13 +786,13 @@ Splice SEP into list of STRINGS, ignoring nil entries. ;;;*** ;;;### (autoloads (proof-toolbar-scripting-menu proof-toolbar-setup) -;;;;;; "proof-toolbar" "proof-toolbar.el" (19107 64554)) +;;;;;; "proof-toolbar" "proof-toolbar.el" (19112 23313)) ;;; Generated autoloads from proof-toolbar.el (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. +Initialize Proof General toolbar and enable it for all PG buffers. +If `proof-toolbar-enable' is nil, change the buffer toolbars +back the default toolbar. \(fn)" t nil) (autoload 'proof-toolbar-toggle "proof-toolbar") @@ -789,22 +804,16 @@ Menu made from the Proof General toolbar commands. ;;;*** -;;;### (autoloads (proof-unicode-tokens-set-global proof-unicode-tokens-enable) -;;;;;; "proof-unicode-tokens" "proof-unicode-tokens.el" (19106 28182)) +;;;### (autoloads (proof-unicode-tokens-set-global proof-unicode-tokens-mode-if-enabled) +;;;;;; "proof-unicode-tokens" "proof-unicode-tokens.el" (19112 23355)) ;;; Generated autoloads from proof-unicode-tokens.el -(autoload 'proof-unicode-tokens-enable "proof-unicode-tokens" "\ -Turn on or off Unicode tokens mode in Proof General script buffer. -This invokes `unicode-tokens-mode' to toggle the setting for the current -buffer, and then sets PG's option for default to match. -Also we arrange to have unicode tokens mode turn itself on automatically -in future if we have just activated it for this buffer. -Note: this function is called when the customize setting for the prover -is changed. +(autoload (quote proof-unicode-tokens-mode-if-enabled) "proof-unicode-tokens" "\ +Turn on or off the Unicode Tokens minor mode in this buffer. -\(fn)" t nil) +\(fn)" nil nil) -(autoload 'proof-unicode-tokens-set-global "proof-unicode-tokens" "\ +(autoload (quote proof-unicode-tokens-set-global) "proof-unicode-tokens" "\ Set global status of unicode tokens mode for PG buffers to be FLAG. Turn on/off menu in all script buffers and ensure new buffers follow suit. @@ -812,8 +821,31 @@ Turn on/off menu in all script buffers and ensure new buffers follow suit. ;;;*** +;;;### (autoloads (defpacustom proof-defpacustom-fn) "proof-utils" +;;;;;; "proof-utils.el" (19112 23313)) +;;; Generated autoloads from proof-utils.el + +(autoload (quote proof-defpacustom-fn) "proof-utils" "\ +As for macro `defpacustom' but evaluating arguments. + +\(fn NAME VAL ARGS)" nil nil) + +(autoload (quote defpacustom) "proof-utils" "\ +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 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. + +\(fn NAME VAL &rest ARGS)" nil (quote macro)) + +;;;*** + ;;;### (autoloads (scomint-make scomint-make-in-buffer) "scomint" -;;;;;; "../lib/scomint.el" (19109 20818)) +;;;;;; "../lib/scomint.el" (19110 10300)) ;;; Generated autoloads from ../lib/scomint.el (autoload 'scomint-make-in-buffer "scomint" "\ @@ -845,10 +877,10 @@ If PROGRAM is a string, any more args are arguments to PROGRAM. ;;;*** ;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "../lib/texi-docstring-magic.el" -;;;;;; (19107 62790)) +;;;;;; (19110 10300)) ;;; Generated autoloads from ../lib/texi-docstring-magic.el -(autoload (quote texi-docstring-magic) "texi-docstring-magic" "\ +(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). @@ -858,10 +890,10 @@ With prefix arg, no errors on unknown symbols. (This results in ;;;*** ;;;### (autoloads (unicode-chars-list-chars) "unicode-chars" "../lib/unicode-chars.el" -;;;;;; (19107 62795)) +;;;;;; (19110 10300)) ;;; Generated autoloads from ../lib/unicode-chars.el -(autoload (quote unicode-chars-list-chars) "unicode-chars" "\ +(autoload 'unicode-chars-list-chars "unicode-chars" "\ Insert each Unicode character into a buffer. Lets you see which characters are available for literal display in your emacs font. @@ -871,10 +903,10 @@ in your emacs font. ;;;*** ;;;### (autoloads (unicode-tokens-encode-str) "unicode-tokens" "../lib/unicode-tokens.el" -;;;;;; (19108 51332)) +;;;;;; (19112 23313)) ;;; Generated autoloads from ../lib/unicode-tokens.el -(autoload 'unicode-tokens-encode-str "unicode-tokens" "\ +(autoload (quote unicode-tokens-encode-str) "unicode-tokens" "\ Return a unicode encoded version presentation of STR. \(fn STR)" nil nil) @@ -885,7 +917,7 @@ Return a unicode encoded version presentation of STR. ;;;;;; "../lib/pg-fontsets.el" "../lib/proof-compat.el" "../lib/span.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") (19109 31686 18792)) +;;;;;; "proof.el" "test.el") (19112 23608 594193)) ;;;*** |