| Index Entry | Section |
|---|
|
| C | | |
|---|
| comment-quote-nested | 9. Configuring Editing Syntax |
|
| I | | |
|---|
| imenu-generic-expression | 3.3 Recognizing other elements |
|
| O | | |
|---|
| outline-heading-end-regexp | 9. Configuring Editing Syntax |
| outline-regexp | 9. Configuring Editing Syntax |
|
| P | | |
|---|
| PA-completion-table | 3.12 Completions |
| PA-help-menu-entries | 2.2 Menu configuration |
| PA-menu-entries | 2.2 Menu configuration |
| PA-prog-args | 4.1 Commands |
| PA-prog-env | 4.1 Commands |
| PA-toolbar-entries | 2.3 Toolbar configuration |
| pbp-goal-command | 5. Goals Buffer Settings |
| pbp-hyp-command | 5. Goals Buffer Settings |
| pg-after-fontify-output-hook | 10. Configuring Font Lock |
| pg-before-fontify-output-hook | 10. Configuring Font Lock |
| pg-goals-change-goal | 5. Goals Buffer Settings |
| pg-goals-error-regexp | 5. Goals Buffer Settings |
| pg-subterm-anns-use-stack | 14.6 Proof shell mode |
| pg-subterm-end-char | 5. Goals Buffer Settings |
| pg-subterm-first-special-char | 4.3 Settings for matching various output from proof process |
| pg-subterm-sep-char | 5. Goals Buffer Settings |
| pg-subterm-start-char | 5. Goals Buffer Settings |
| pg-topterm-goalhyplit-fn | 3.4 Configuring undo behaviour |
| pg-topterm-regexp | 5. Goals Buffer Settings |
| proof-action-list | 14.6 Proof shell mode |
| proof-action-list | 14.6.1 Input to the shell |
| proof-action-list | 14.6.2 Output from the shell |
| proof-activate-scripting-hook | 3.9 Activate scripting hook |
| proof-assistant-home-page | 2.1 Settings for generic user-level commands |
| proof-assistant-table | 1.1 Overview of adding a new prover |
| proof-assistants | 14.2 Proof General site configuration |
| proof-atomic-sequents-list | A.2 Granularity of atomic command sequences |
| proof-auto-multiple-files | 3.10 Automatic multiple files |
| proof-buffer-type | 14.4 Global variables |
| proof-cannot-reopen-processed-files | 4.4 Settings for matching urgent messages from proof process |
| proof-cannot-reopen-processed-files | 8. Handling Multiple Files |
| proof-case-fold-search | 3.1 Recognizing commands and comments |
| proof-completed-proof-behaviour | 3.2 Recognizing proofs |
| proof-context-command | 2.1 Settings for generic user-level commands |
| proof-count-undos-fn | 3.4 Configuring undo behaviour |
| proof-electric-terminator-noterminator | 3.1 Recognizing commands and comments |
| proof-find-and-forget-fn | 3.4 Configuring undo behaviour |
| proof-find-theorems-command | 2.1 Settings for generic user-level commands |
| proof-forget-id-command | 3.4 Configuring undo behaviour |
| proof-general-debug | 14.7 Debugging |
| proof-general-home-page | 7. Global Constants |
| proof-general-name | 7. Global Constants |
| proof-general-version | 14.2 Proof General site configuration |
| proof-get-proof-info-fn | 3.7 Proof status statistic |
| proof-goal-command | 2.1 Settings for generic user-level commands |
| proof-goal-command-p | 3.2 Recognizing proofs |
| proof-goal-command-regexp | 3.2 Recognizing proofs |
| proof-goal-with-hole-regexp | 3.2 Recognizing proofs |
| proof-goal-with-hole-regexp | 3.3 Recognizing other elements |
| proof-goal-with-hole-result | 3.2 Recognizing proofs |
| proof-goal-with-hole-result | 3.3 Recognizing other elements |
| proof-goals-buffer | 14.4 Global variables |
| proof-goals-font-lock-keywords | 10. Configuring Font Lock |
| proof-home-directory | 14.2 Proof General site configuration |
| proof-ignore-for-undo-count | 3.4 Configuring undo behaviour |
| proof-images-directory | 14.2 Proof General site configuration |
| proof-included-files-list | 4.4 Settings for matching urgent messages from proof process |
| proof-included-files-list | 4.4 Settings for matching urgent messages from proof process |
| proof-included-files-list | 8. Handling Multiple Files |
| proof-included-files-list | 14.4 Global variables |
| proof-info-command | 2.1 Settings for generic user-level commands |
| proof-info-directory | 14.2 Proof General site configuration |
| proof-kill-goal-command | 3.4 Configuring undo behaviour |
| proof-locked-span | 14.5 Proof script mode |
| proof-marker | 14.6 Proof shell mode |
| proof-nested-goals-history-p | 3.5 Nested proofs |
| proof-nested-undo-regexp | 3.5 Nested proofs |
| proof-no-fully-processed-buffer | 3.11 Completely asserted buffers |
| proof-non-undoables-regexp | 3.4 Configuring undo behaviour |
| proof-omit-cheating-regexp | 3.7 Proof status statistic |
| proof-omit-proofs-configured | 3.6 Omitting proofs for speed |
| proof-prog-name | 4.1 Commands |
| proof-queue-span | 14.5 Proof script mode |
| proof-really-save-command-p | 3.2 Recognizing proofs |
| proof-response-buffer | 14.4 Global variables |
| proof-response-font-lock-keywords | 10. Configuring Font Lock |
| proof-retract-command-fn | 3.7 Proof status statistic |
| proof-save-command | 2.1 Settings for generic user-level commands |
| proof-save-command-regexp | 3.2 Recognizing proofs |
| proof-save-with-hole-regexp | 3.2 Recognizing proofs |
| proof-script-buffer | 14.4 Global variables |
| proof-script-cmd-force-next-proof-kept | 3.6 Omitting proofs for speed |
| proof-script-cmd-prevents-proof-omission | 3.6 Omitting proofs for speed |
| proof-script-command-end-regexp | 3.1 Recognizing commands and comments |
| proof-script-command-start-regexp | 3.1 Recognizing commands and comments |
| proof-script-comment-end | 3.1 Recognizing commands and comments |
| proof-script-comment-end-regexp | 3.1 Recognizing commands and comments |
| proof-script-comment-start | 3.1 Recognizing commands and comments |
| proof-script-comment-start-regexp | 3.1 Recognizing commands and comments |
| proof-script-definition-end-regexp | 3.6 Omitting proofs for speed |
| proof-script-font-lock-keywords | 10. Configuring Font Lock |
| proof-script-imenu-generic-expression | 3.3 Recognizing other elements |
| proof-script-proof-admit-command | 3.6 Omitting proofs for speed |
| proof-script-proof-end-regexp | 3.6 Omitting proofs for speed |
| proof-script-proof-start-regexp | 3.6 Omitting proofs for speed |
| proof-script-sexp-commands | 3.1 Recognizing commands and comments |
| proof-script-syntax-table-entries | 9. Configuring Editing Syntax |
| proof-second-action-list-active | 14.6 Proof shell mode |
| proof-shell-annotated-prompt-regexp | 4.3 Settings for matching various output from proof process |
| proof-shell-assumption-regexp | 4.3 Settings for matching various output from proof process |
| proof-shell-auto-terminate-commands | 4.1 Commands |
| proof-shell-buffer | 14.4 Global variables |
| proof-shell-busy | 14.6 Proof shell mode |
| proof-shell-cd-cmd | 4.1 Commands |
| proof-shell-clear-goals-regexp | 4.4 Settings for matching urgent messages from proof process |
| proof-shell-clear-response-regexp | 4.4 Settings for matching urgent messages from proof process |
| proof-shell-compute-new-files-list | 4.4 Settings for matching urgent messages from proof process |
| proof-shell-compute-new-files-list | 8. Handling Multiple Files |
| proof-shell-delayed-output-end | 14.6.2 Output from the shell |
| proof-shell-delayed-output-flags | 14.6.2 Output from the shell |
| proof-shell-delayed-output-start | 14.6.2 Output from the shell |
| proof-shell-eager-annotation-end | 4.4 Settings for matching urgent messages from proof process |
| proof-shell-eager-annotation-end | 8. Handling Multiple Files |
| proof-shell-eager-annotation-start | 4.4 Settings for matching urgent messages from proof process |
| proof-shell-eager-annotation-start | 8. Handling Multiple Files |
| proof-shell-eager-annotation-start-length | 4.4 Settings for matching urgent messages from proof process |
| proof-shell-end-goals-regexp | 4.3 Settings for matching various output from proof process |
| proof-shell-error-or-interrupt-seen | 14.4 Global variables |
| proof-shell-error-regexp | 4.3 Settings for matching various output from proof process |
| proof-shell-filename-escapes | 4.5 Hooks and other settings |
| proof-shell-handle-error-or-interrupt-hook | 4.5 Hooks and other settings |
| proof-shell-handle-output-system-specific | 4.5 Hooks and other settings |
| proof-shell-inform-file-processed-cmd | 4.1 Commands |
| proof-shell-inform-file-retracted-cmd | 4.1 Commands |
| proof-shell-init-cmd | 4.1 Commands |
| proof-shell-insert-hook | 4.2 Script input to the shell |
| proof-shell-interactive-prompt-regexp | 4.4 Settings for matching urgent messages from proof process |
| proof-shell-interrupt-regexp | 4.3 Settings for matching various output from proof process |
| proof-shell-last-output | 14.6.2 Output from the shell |
| proof-shell-last-output-kind | 14.6.2 Output from the shell |
| proof-shell-last-output-kind | 14.6.2 Output from the shell |
| proof-shell-last-prompt | 14.6.2 Output from the shell |
| proof-shell-old-proof-marker-position | 14.6 Proof shell mode |
| proof-shell-pre-interrupt-hook | 4.5 Hooks and other settings |
| proof-shell-pre-sync-init-cmd | 4.1 Commands |
| proof-shell-process-connection-type | 4.5 Hooks and other settings |
| proof-shell-process-file | 4.4 Settings for matching urgent messages from proof process |
| proof-shell-process-file | 8. Handling Multiple Files |
| proof-shell-proof-completed | 14.4 Global variables |
| proof-shell-proof-completed-regexp | 4.3 Settings for matching various output from proof process |
| proof-shell-quit-cmd | 4.1 Commands |
| proof-shell-restart-cmd | 4.1 Commands |
| proof-shell-result-end | 5. Goals Buffer Settings |
| proof-shell-result-start | 5. Goals Buffer Settings |
| proof-shell-retract-files-regexp | 4.4 Settings for matching urgent messages from proof process |
| proof-shell-retract-files-regexp | 8. Handling Multiple Files |
| proof-shell-silent-threshold | 4.1 Commands |
| proof-shell-start-goals-regexp | 4.3 Settings for matching various output from proof process |
| proof-shell-start-silent-cmd | 4.1 Commands |
| proof-shell-stop-silent-cmd | 4.1 Commands |
| proof-shell-strip-crs-from-input | 4.2 Script input to the shell |
| proof-shell-strip-crs-from-output | 14.6.2 Output from the shell |
| proof-shell-syntax-table-entries | 9. Configuring Editing Syntax |
| proof-shell-theorem-dependency-list-regexp | 4.4 Settings for matching urgent messages from proof process |
| proof-shell-trace-output-regexp | 4.4 Settings for matching urgent messages from proof process |
| proof-shell-truncate-before-error | 4.3 Settings for matching various output from proof process |
| proof-shell-urgent-message-marker | 14.6.2 Output from the shell |
| proof-showproof-command | 2.1 Settings for generic user-level commands |
| proof-splash-contents | 6. Splash Screen Settings |
| proof-splash-time | 6. Splash Screen Settings |
| proof-state-preserving-p | 3.8 Safe (state-preserving) commands |
| proof-terminal-string | 3.1 Recognizing commands and comments |
| proof-tokens-activate-command | 11. Configuring Tokens |
| proof-tokens-deactivate-command | 11. Configuring Tokens |
| proof-tokens-extra-modes | 11. Configuring Tokens |
| proof-toolbar-entries-default | 2.3 Toolbar configuration |
| proof-tree-configured | 12.3.3 Guards |
| proof-tree-external-display | 12.3.3 Guards |
| proof-undo-n-times-cmd | 3.4 Configuring undo behaviour |
| proof-universal-keys | 7. Global Constants |
|