diff options
Diffstat (limited to 'generic/proof-autoloads.el')
-rw-r--r-- | generic/proof-autoloads.el | 146 |
1 files changed, 96 insertions, 50 deletions
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el index 53338267..f618b0c9 100644 --- a/generic/proof-autoloads.el +++ b/generic/proof-autoloads.el @@ -8,7 +8,7 @@ ;;;*** ;;;### (autoloads (bufhist-mode bufhist-exit bufhist-init) "bufhist" -;;;;;; "../lib/bufhist.el" (19096 4063)) +;;;;;; "../lib/bufhist.el" (19106 28183)) ;;; Generated autoloads from ../lib/bufhist.el (autoload 'bufhist-init "bufhist" "\ @@ -40,8 +40,8 @@ Commands:\\<bufhist-minor-mode-map> ;;;*** ;;;### (autoloads (holes-mode holes-insert-and-expand holes-abbrev-complete -;;;;;; holes-set-make-active-hole) "holes" "../lib/holes.el" (18971 -;;;;;; 55597)) +;;;;;; holes-set-make-active-hole) "holes" "../lib/holes.el" (19106 +;;;;;; 28183)) ;;; Generated autoloads from ../lib/holes.el (autoload 'holes-set-make-active-hole "holes" "\ @@ -72,7 +72,7 @@ turn it off. ;;;*** ;;;### (autoloads (maths-menu-mode) "maths-menu" "../lib/maths-menu.el" -;;;;;; (19074 48881)) +;;;;;; (19106 28183)) ;;; Generated autoloads from ../lib/maths-menu.el (autoload 'maths-menu-mode "maths-menu" "\ @@ -86,7 +86,7 @@ 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" (18971 55596)) +;;;;;; "pg-assoc" "pg-assoc.el" (19106 28180)) ;;; Generated autoloads from pg-assoc.el (autoload 'proof-associated-buffers "pg-assoc" "\ @@ -104,7 +104,7 @@ Dead or nil buffers are not represented in the list. ;;;*** ;;;### (autoloads (proof-goals-config-done) "pg-goals" "pg-goals.el" -;;;;;; (19056 25870)) +;;;;;; (19106 28181)) ;;; Generated autoloads from pg-goals.el (autoload 'proof-goals-config-done "pg-goals" "\ @@ -115,7 +115,7 @@ 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" (19074 48879)) +;;;;;; "pg-pgip" "pg-pgip.el" (19106 28181)) ;;; Generated autoloads from pg-pgip.el (autoload 'pg-pgip-process-packet "pg-pgip" "\ @@ -138,8 +138,8 @@ 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" (19056 -;;;;;; 25870)) +;;;;;; proof-response-mode) "pg-response" "pg-response.el" (19106 +;;;;;; 28181)) ;;; Generated autoloads from pg-response.el (autoload 'proof-response-mode "pg-response" "\ @@ -192,7 +192,7 @@ See `pg-next-error-regexp'. ;;;*** ;;;### (autoloads (pg-defthymode) "pg-thymodes" "pg-thymodes.el" -;;;;;; (18971 55596)) +;;;;;; (19106 28181)) ;;; Generated autoloads from pg-thymodes.el (autoload 'pg-defthymode "pg-thymodes" "\ @@ -216,10 +216,9 @@ All of these settings are optional. ;;;;;; pg-add-to-input-history pg-next-matching-input-from-input ;;;;;; 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-term-incomment-fn -;;;;;; proof-electric-terminator-enable proof-define-assistant-command-witharg -;;;;;; proof-define-assistant-command) "pg-user" "pg-user.el" (19085 -;;;;;; 10018)) +;;;;;; 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" (19106 28181)) ;;; Generated autoloads from pg-user.el (autoload 'proof-define-assistant-command "pg-user" "\ @@ -239,11 +238,6 @@ Make sure the modeline is updated to display new value for electric terminator. \(fn)" nil nil) -(autoload 'proof-electric-term-incomment-fn "pg-user" "\ -Used as argument to `proof-assert-until-point'. - -\(fn)" nil nil) - (autoload 'pg-slow-fontify-tracing-hint "pg-user" "\ Not documented @@ -317,8 +311,8 @@ Not documented ;;;*** -;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (18971 -;;;;;; 55596)) +;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (19106 +;;;;;; 28181)) ;;; Generated autoloads from pg-xml.el (autoload 'pg-xml-parse-string "pg-xml" "\ @@ -329,7 +323,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" (18971 55596)) +;;;;;; "proof-depends" "proof-depends.el" (19106 28181)) ;;; Generated autoloads from proof-depends.el (autoload 'proof-depends-process-dependencies "proof-depends" "\ @@ -347,7 +341,7 @@ Make a portion of a context-sensitive menu showing proof dependencies. ;;;*** ;;;### (autoloads (proof-easy-config) "proof-easy-config" "proof-easy-config.el" -;;;;;; (18971 55596)) +;;;;;; (19106 28181)) ;;; Generated autoloads from proof-easy-config.el (autoload 'proof-easy-config "proof-easy-config" "\ @@ -360,7 +354,7 @@ the `proof-assistant-table', which see. ;;;*** ;;;### (autoloads (proof-indent-line) "proof-indent" "proof-indent.el" -;;;;;; (18971 55596)) +;;;;;; (19106 28181)) ;;; Generated autoloads from proof-indent.el (autoload 'proof-indent-line "proof-indent" "\ @@ -371,7 +365,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" (18971 55596)) +;;;;;; "proof-maths-menu" "proof-maths-menu.el" (19106 28181)) ;;; Generated autoloads from proof-maths-menu.el (autoload 'proof-maths-menu-set-global "proof-maths-menu" "\ @@ -393,7 +387,7 @@ 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" (19092 9335)) +;;;;;; "proof-menu" "proof-menu.el" (19106 28181)) ;;; Generated autoloads from proof-menu.el (autoload 'proof-menu-define-keys "proof-menu" "\ @@ -436,7 +430,7 @@ evaluate can be provided instead. ;;;*** ;;;### (autoloads (proof-mmm-enable proof-mmm-set-global) "proof-mmm" -;;;;;; "proof-mmm.el" (18971 55596)) +;;;;;; "proof-mmm.el" (19106 28181)) ;;; Generated autoloads from proof-mmm.el (autoload 'proof-mmm-set-global "proof-mmm" "\ @@ -458,8 +452,8 @@ 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" (19096 -;;;;;; 3913)) +;;;;;; proof-colour-locked) "proof-script" "proof-script.el" (19106 +;;;;;; 28915)) ;;; Generated autoloads from proof-script.el (autoload 'proof-colour-locked "proof-script" "\ @@ -492,7 +486,7 @@ Non-nil if the locked region is empty. Works on any buffer. (autoload 'pg-set-span-helphighlights "proof-script" "\ Add a daughter help span for SPAN with help message, highlight, actions. -We add the last output to the hover display here. +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) @@ -525,8 +519,8 @@ finish setup which depends on specific proof assistant configuration. ;;;### (autoloads (proof-shell-config-done proof-shell-mode proof-shell-invisible-command-invisible-result ;;;;;; 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-live-buffer proof-shell-ready-prover) -;;;;;; "proof-shell" "proof-shell.el" (19096 3825)) +;;;;;; proof-shell-available-p proof-shell-ready-prover) "proof-shell" +;;;;;; "proof-shell.el" (19106 28181)) ;;; Generated autoloads from proof-shell.el (autoload 'proof-shell-ready-prover "proof-shell" "\ @@ -538,10 +532,8 @@ No change to current buffer or point. \(fn &optional QUEUEMODE)" nil nil) -(autoload 'proof-shell-live-buffer "proof-shell" "\ -Return buffer of active proof assistant, or nil if none running. - -\(fn)" nil nil) +(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" "\ Return non-nil if there is a proof shell active and available. @@ -550,7 +542,7 @@ No error messages. Useful as menu or toolbar enabler. \(fn)" nil nil) (autoload 'proof-shell-insert "proof-shell" "\ -Insert STRING at the end of the proof shell, call `comint-send-input'. +Insert STRING at the end of the proof shell, call `scomint-send-input'. First we call `proof-shell-insert-hook'. The arguments `action' and `scriptspan' may be examined by the hook to determine how to modify @@ -645,15 +637,25 @@ processing. ;;;*** +;;;### (autoloads (proof-ready-for-assistant) "proof-site" "proof-site.el" +;;;;;; (19106 28181)) +;;; Generated autoloads from proof-site.el + +(autoload 'proof-ready-for-assistant "proof-site" "\ +Configure PG for symbol ASSISTANTSYM, name ASSISTANT-NAME. +If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'. + +\(fn ASSISTANTSYM &optional ASSISTANT-NAME)" nil nil) + +;;;*** + ;;;### (autoloads (proof-splash-message proof-splash-display-screen) -;;;;;; "proof-splash" "proof-splash.el" (18971 55597)) +;;;;;; "proof-splash" "proof-splash.el" (19106 28181)) ;;; Generated autoloads from proof-splash.el (autoload '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. +If TIMEOUT is non-nil, arrange for a time-out to occur outside this function. \(fn &optional TIMEOUT)" t nil) @@ -665,7 +667,7 @@ Make sure the user gets welcomed one way or another. ;;;*** ;;;### (autoloads (proof-splice-separator proof-format) "proof-syntax" -;;;;;; "proof-syntax.el" (19085 10019)) +;;;;;; "proof-syntax.el" (19106 28181)) ;;; Generated autoloads from proof-syntax.el (autoload 'proof-format "proof-syntax" "\ @@ -683,7 +685,7 @@ Splice SEP into list of STRINGS, ignoring nil entries. ;;;*** ;;;### (autoloads (proof-toolbar-scripting-menu proof-toolbar-setup) -;;;;;; "proof-toolbar" "proof-toolbar.el" (19085 10019)) +;;;;;; "proof-toolbar" "proof-toolbar.el" (19106 28182)) ;;; Generated autoloads from proof-toolbar.el (autoload 'proof-toolbar-setup "proof-toolbar" "\ @@ -702,7 +704,7 @@ 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" (19075 7791)) +;;;;;; "proof-unicode-tokens" "proof-unicode-tokens.el" (19106 28182)) ;;; Generated autoloads from proof-unicode-tokens.el (autoload 'proof-unicode-tokens-enable "proof-unicode-tokens" "\ @@ -724,8 +726,40 @@ 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" (19106 12942)) +;;; Generated autoloads from ../lib/scomint.el + +(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 +via `start-file-process', or a cons pair of the form (HOST . SERVICE) denoting +a TCP connection to be opened via `open-network-stream'. If there is already +a running process in that buffer, it is not restarted. Optional fourth arg +STARTFILE is the name of a file to send the contents of to the process. + +If PROGRAM is a string, any more args are arguments to PROGRAM. + +\(fn NAME BUFFER PROGRAM &optional STARTFILE &rest SWITCHES)" nil nil) + +(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 +via `start-file-process', or a cons pair of the form (HOST . SERVICE) denoting +a TCP connection to be opened via `open-network-stream'. If there is already +a running process in that buffer, it is not restarted. Optional third arg +STARTFILE is the name of a file to send the contents of the process to. + +If PROGRAM is a string, any more args are arguments to PROGRAM. + +\(fn NAME PROGRAM &optional STARTFILE &rest SWITCHES)" nil nil) + +;;;*** + ;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "../lib/texi-docstring-magic.el" -;;;;;; (18971 55597)) +;;;;;; (19106 28184)) ;;; Generated autoloads from ../lib/texi-docstring-magic.el (autoload 'texi-docstring-magic "texi-docstring-magic" "\ @@ -737,13 +771,25 @@ With prefix arg, no errors on unknown symbols. (This results in ;;;*** +;;;### (autoloads (unicode-chars-list-chars) "unicode-chars" "../lib/unicode-chars.el" +;;;;;; (19106 32184)) +;;; Generated autoloads from ../lib/unicode-chars.el + +(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. + +\(fn)" t 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-chars.el" "../lib/unicode-tokens.el" "comptest.el" -;;;;;; "pg-autotest.el" "pg-custom.el" "pg-pbrpm.el" "pg-span.el" -;;;;;; "pg-vars.el" "proof-auxmodes.el" "proof-config.el" "proof-faces.el" -;;;;;; "proof-site.el" "proof-useropts.el" "proof-utils.el" "proof.el") -;;;;;; (19096 4069 299056)) +;;;;;; "../lib/unicode-tokens.el" "comptest.el" "pg-autotest.el" +;;;;;; "pg-custom.el" "pg-pbrpm.el" "pg-span.el" "pg-vars.el" "proof-auxmodes.el" +;;;;;; "proof-config.el" "proof-faces.el" "proof-useropts.el" "proof-utils.el" +;;;;;; "proof.el") (19106 44543 93145)) ;;;*** |