---

Function and Command Index

Jump to:	D   P

	Index Entry	Section
D
	defpgcustom	14.3 Configuration variable mechanisms
	defpgdefault	13.1 Default values for generic settings
	defpgdefault	14.3 Configuration variable mechanisms
P
	proof-activate-scripting	14.5 Proof script mode
	proof-add-completions	3.12 Completions
	proof-ass	14.3 Configuration variable mechanisms
	proof-ass-sym	14.3 Configuration variable mechanisms
	proof-ass-symv	14.3 Configuration variable mechanisms
	proof-assert-until-point	14.5 Proof script mode
	proof-complete-buffer-atomic	14.5 Proof script mode
	proof-deactivate-scripting	14.5 Proof script mode
	proof-define-assistant-command	13.4 Useful functions and macros
	proof-define-assistant-command-witharg	13.4 Useful functions and macros
	proof-definvisible	13.4 Useful functions and macros
	proof-defshortcut	13.4 Useful functions and macros
	proof-deftoggle	14.3 Configuration variable mechanisms
	proof-extend-queue	14.6.1 Input to the shell
	proof-extend-queue	14.6.1 Input to the shell
	proof-format-filename	13.4 Useful functions and macros
	proof-generic-count-undos	3.4 Configuring undo behaviour
	proof-generic-find-and-forget	3.4 Configuring undo behaviour
	proof-generic-state-preserving-p	3.8 Safe (state-preserving) commands
	proof-grab-lock	14.6.1 Input to the shell
	proof-init-segmentation	14.5 Proof script mode
	proof-insert	13.4 Useful functions and macros
	proof-looking-at-syntactic-context	3.1 Recognizing commands and comments
	proof-register-possibly-new-processed-file	14.5 Proof script mode
	proof-release-lock	14.6.1 Input to the shell
	proof-restart-buffers	14.5 Proof script mode
	proof-retract-until-point	14.5 Proof script mode
	proof-script-generic-parse-cmdend	14.5 Proof script mode
	proof-script-generic-parse-cmdstart	14.5 Proof script mode
	proof-script-generic-parse-sexp	14.5 Proof script mode
	proof-script-remove-all-spans-and-deactivate	14.5 Proof script mode
	proof-semis-to-vanillas	14.5 Proof script mode
	proof-set-value	14.3 Configuration variable mechanisms
	proof-shell-bail-out	14.6 Proof shell mode
	proof-shell-exec-loop	14.6.1 Input to the shell
	proof-shell-exit	14.6 Proof shell mode
	proof-shell-filter	14.6.2 Output from the shell
	proof-shell-filter-manage-output	14.6.2 Output from the shell
	proof-shell-filter-wrapper	14.6.2 Output from the shell
	proof-shell-handle-delayed-output	14.6.2 Output from the shell
	proof-shell-handle-immediate-output	14.6.2 Output from the shell
	proof-shell-insert	14.6.1 Input to the shell
	proof-shell-invisible-command	13.4 Useful functions and macros
	proof-shell-kill-function	14.6 Proof shell mode
	proof-shell-process-urgent-message	14.6.2 Output from the shell
	proof-shell-restart	14.6 Proof shell mode
	proof-shell-start	14.6 Proof shell mode
	proof-tree-external-display-toggle	12.3.3 Guards
	proof-tree-handle-delayed-output	12.3.4 Urgent and Delayed Actions
	proof-tree-urgent-action	12.3.4 Urgent and Delayed Actions
	proof-zap-commas	10. Configuring Font Lock

Jump to:	D   P

---

This document was generated on June 23, 2025 using texi2html 1.82.