[ << ] [ >> ] [Top] [Contents] [Index] [ ? ]

Variable and User Option Index

Jump to:   C   I   O   P  
Index Entry Section
C
comment-quote-nested9. Configuring Editing Syntax
I
imenu-generic-expression3.3 Recognizing other elements
O
outline-heading-end-regexp9. Configuring Editing Syntax
outline-regexp9. Configuring Editing Syntax
P
PA-completion-table3.12 Completions
PA-help-menu-entries2.2 Menu configuration
PA-menu-entries2.2 Menu configuration
PA-prog-args4.1 Commands
PA-prog-env4.1 Commands
PA-toolbar-entries2.3 Toolbar configuration
pbp-goal-command5. Goals Buffer Settings
pbp-hyp-command5. Goals Buffer Settings
pg-after-fontify-output-hook10. Configuring Font Lock
pg-before-fontify-output-hook10. Configuring Font Lock
pg-goals-change-goal5. Goals Buffer Settings
pg-goals-error-regexp5. Goals Buffer Settings
pg-subterm-anns-use-stack14.6 Proof shell mode
pg-subterm-end-char5. Goals Buffer Settings
pg-subterm-first-special-char4.3 Settings for matching various output from proof process
pg-subterm-sep-char5. Goals Buffer Settings
pg-subterm-start-char5. Goals Buffer Settings
pg-topterm-goalhyplit-fn3.4 Configuring undo behaviour
pg-topterm-regexp5. Goals Buffer Settings
proof-action-list14.6 Proof shell mode
proof-action-list14.6.1 Input to the shell
proof-action-list14.6.2 Output from the shell
proof-activate-scripting-hook3.9 Activate scripting hook
proof-assistant-home-page2.1 Settings for generic user-level commands
proof-assistant-table1.1 Overview of adding a new prover
proof-assistants14.2 Proof General site configuration
proof-atomic-sequents-listA.2 Granularity of atomic command sequences
proof-auto-multiple-files3.10 Automatic multiple files
proof-buffer-type14.4 Global variables
proof-cannot-reopen-processed-files4.4 Settings for matching urgent messages from proof process
proof-cannot-reopen-processed-files8. Handling Multiple Files
proof-case-fold-search3.1 Recognizing commands and comments
proof-completed-proof-behaviour3.2 Recognizing proofs
proof-context-command2.1 Settings for generic user-level commands
proof-count-undos-fn3.4 Configuring undo behaviour
proof-electric-terminator-noterminator3.1 Recognizing commands and comments
proof-find-and-forget-fn3.4 Configuring undo behaviour
proof-find-theorems-command2.1 Settings for generic user-level commands
proof-forget-id-command3.4 Configuring undo behaviour
proof-general-debug14.7 Debugging
proof-general-home-page7. Global Constants
proof-general-name7. Global Constants
proof-general-version14.2 Proof General site configuration
proof-get-proof-info-fn3.7 Proof status statistic
proof-goal-command2.1 Settings for generic user-level commands
proof-goal-command-p3.2 Recognizing proofs
proof-goal-command-regexp3.2 Recognizing proofs
proof-goal-with-hole-regexp3.2 Recognizing proofs
proof-goal-with-hole-regexp3.3 Recognizing other elements
proof-goal-with-hole-result3.2 Recognizing proofs
proof-goal-with-hole-result3.3 Recognizing other elements
proof-goals-buffer14.4 Global variables
proof-goals-font-lock-keywords10. Configuring Font Lock
proof-home-directory14.2 Proof General site configuration
proof-ignore-for-undo-count3.4 Configuring undo behaviour
proof-images-directory14.2 Proof General site configuration
proof-included-files-list4.4 Settings for matching urgent messages from proof process
proof-included-files-list4.4 Settings for matching urgent messages from proof process
proof-included-files-list8. Handling Multiple Files
proof-included-files-list14.4 Global variables
proof-info-command2.1 Settings for generic user-level commands
proof-info-directory14.2 Proof General site configuration
proof-kill-goal-command3.4 Configuring undo behaviour
proof-locked-span14.5 Proof script mode
proof-marker14.6 Proof shell mode
proof-nested-goals-history-p3.5 Nested proofs
proof-nested-undo-regexp3.5 Nested proofs
proof-no-fully-processed-buffer3.11 Completely asserted buffers
proof-non-undoables-regexp3.4 Configuring undo behaviour
proof-omit-cheating-regexp3.7 Proof status statistic
proof-omit-proofs-configured3.6 Omitting proofs for speed
proof-prog-name4.1 Commands
proof-queue-span14.5 Proof script mode
proof-really-save-command-p3.2 Recognizing proofs
proof-response-buffer14.4 Global variables
proof-response-font-lock-keywords10. Configuring Font Lock
proof-retract-command-fn3.7 Proof status statistic
proof-save-command2.1 Settings for generic user-level commands
proof-save-command-regexp3.2 Recognizing proofs
proof-save-with-hole-regexp3.2 Recognizing proofs
proof-script-buffer14.4 Global variables
proof-script-cmd-force-next-proof-kept3.6 Omitting proofs for speed
proof-script-cmd-prevents-proof-omission3.6 Omitting proofs for speed
proof-script-command-end-regexp3.1 Recognizing commands and comments
proof-script-command-start-regexp3.1 Recognizing commands and comments
proof-script-comment-end3.1 Recognizing commands and comments
proof-script-comment-end-regexp3.1 Recognizing commands and comments
proof-script-comment-start3.1 Recognizing commands and comments
proof-script-comment-start-regexp3.1 Recognizing commands and comments
proof-script-definition-end-regexp3.6 Omitting proofs for speed
proof-script-font-lock-keywords10. Configuring Font Lock
proof-script-imenu-generic-expression3.3 Recognizing other elements
proof-script-proof-admit-command3.6 Omitting proofs for speed
proof-script-proof-end-regexp3.6 Omitting proofs for speed
proof-script-proof-start-regexp3.6 Omitting proofs for speed
proof-script-sexp-commands3.1 Recognizing commands and comments
proof-script-syntax-table-entries9. Configuring Editing Syntax
proof-second-action-list-active14.6 Proof shell mode
proof-shell-annotated-prompt-regexp4.3 Settings for matching various output from proof process
proof-shell-assumption-regexp4.3 Settings for matching various output from proof process
proof-shell-auto-terminate-commands4.1 Commands
proof-shell-buffer14.4 Global variables
proof-shell-busy14.6 Proof shell mode
proof-shell-cd-cmd4.1 Commands
proof-shell-clear-goals-regexp4.4 Settings for matching urgent messages from proof process
proof-shell-clear-response-regexp4.4 Settings for matching urgent messages from proof process
proof-shell-compute-new-files-list4.4 Settings for matching urgent messages from proof process
proof-shell-compute-new-files-list8. Handling Multiple Files
proof-shell-delayed-output-end14.6.2 Output from the shell
proof-shell-delayed-output-flags14.6.2 Output from the shell
proof-shell-delayed-output-start14.6.2 Output from the shell
proof-shell-eager-annotation-end4.4 Settings for matching urgent messages from proof process
proof-shell-eager-annotation-end8. Handling Multiple Files
proof-shell-eager-annotation-start4.4 Settings for matching urgent messages from proof process
proof-shell-eager-annotation-start8. Handling Multiple Files
proof-shell-eager-annotation-start-length4.4 Settings for matching urgent messages from proof process
proof-shell-end-goals-regexp4.3 Settings for matching various output from proof process
proof-shell-error-or-interrupt-seen14.4 Global variables
proof-shell-error-regexp4.3 Settings for matching various output from proof process
proof-shell-filename-escapes4.5 Hooks and other settings
proof-shell-handle-error-or-interrupt-hook4.5 Hooks and other settings
proof-shell-handle-output-system-specific4.5 Hooks and other settings
proof-shell-inform-file-processed-cmd4.1 Commands
proof-shell-inform-file-retracted-cmd4.1 Commands
proof-shell-init-cmd4.1 Commands
proof-shell-insert-hook4.2 Script input to the shell
proof-shell-interactive-prompt-regexp4.4 Settings for matching urgent messages from proof process
proof-shell-interrupt-regexp4.3 Settings for matching various output from proof process
proof-shell-last-output14.6.2 Output from the shell
proof-shell-last-output-kind14.6.2 Output from the shell
proof-shell-last-output-kind14.6.2 Output from the shell
proof-shell-last-prompt14.6.2 Output from the shell
proof-shell-old-proof-marker-position14.6 Proof shell mode
proof-shell-pre-interrupt-hook4.5 Hooks and other settings
proof-shell-pre-sync-init-cmd4.1 Commands
proof-shell-process-connection-type4.5 Hooks and other settings
proof-shell-process-file4.4 Settings for matching urgent messages from proof process
proof-shell-process-file8. Handling Multiple Files
proof-shell-proof-completed14.4 Global variables
proof-shell-proof-completed-regexp4.3 Settings for matching various output from proof process
proof-shell-quit-cmd4.1 Commands
proof-shell-restart-cmd4.1 Commands
proof-shell-result-end5. Goals Buffer Settings
proof-shell-result-start5. Goals Buffer Settings
proof-shell-retract-files-regexp4.4 Settings for matching urgent messages from proof process
proof-shell-retract-files-regexp8. Handling Multiple Files
proof-shell-silent-threshold4.1 Commands
proof-shell-start-goals-regexp4.3 Settings for matching various output from proof process
proof-shell-start-silent-cmd4.1 Commands
proof-shell-stop-silent-cmd4.1 Commands
proof-shell-strip-crs-from-input4.2 Script input to the shell
proof-shell-strip-crs-from-output14.6.2 Output from the shell
proof-shell-syntax-table-entries9. Configuring Editing Syntax
proof-shell-theorem-dependency-list-regexp4.4 Settings for matching urgent messages from proof process
proof-shell-trace-output-regexp4.4 Settings for matching urgent messages from proof process
proof-shell-truncate-before-error4.3 Settings for matching various output from proof process
proof-shell-urgent-message-marker14.6.2 Output from the shell
proof-showproof-command2.1 Settings for generic user-level commands
proof-splash-contents6. Splash Screen Settings
proof-splash-time6. Splash Screen Settings
proof-state-preserving-p3.8 Safe (state-preserving) commands
proof-terminal-string3.1 Recognizing commands and comments
proof-tokens-activate-command11. Configuring Tokens
proof-tokens-deactivate-command11. Configuring Tokens
proof-tokens-extra-modes11. Configuring Tokens
proof-toolbar-entries-default2.3 Toolbar configuration
proof-tree-configured12.3.3 Guards
proof-tree-external-display12.3.3 Guards
proof-undo-n-times-cmd3.4 Configuring undo behaviour
proof-universal-keys7. Global Constants
Jump to:   C   I   O   P  
[ << ] [ >> ] [Top] [Contents] [Index] [ ? ]

This document was generated on November 20, 2025 using texi2html 1.82.