diff options
| -rw-r--r-- | coq/coq.el | 3 | ||||
| -rw-r--r-- | generic/proof-config.el | 19 |
2 files changed, 22 insertions, 0 deletions
@@ -445,6 +445,9 @@ (setq proof-auto-multiple-files t) ; until Coq has real support + (setq proof-shell-start-silent-cmd "Begin Silent" + proof-shell-stop-silent-cmd "End Silent") + (coq-init-syntax-table) ;; font-lock diff --git a/generic/proof-config.el b/generic/proof-config.el index 11005b62..fb4ac34a 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1207,6 +1207,25 @@ Proof General about the dependencies rather than using this setting." :type 'boolean :group 'proof-shell) +(defcustom proof-shell-start-silent-cmd nil + "Command to turn prover goals output off when sending many script commands. +If non-nil, Proof General will automatically issue this command +to help speed up processing of long proof scripts. +See also proof-shell-stop-silent-cmd. +NOT IMPLEMENTED YET. Forthcoming in next version." + :type '(choice string (const nil)) + :group 'proof-shell) + +(defcustom proof-shell-stop-silent-cmd nil + "Command to turn prover output on. +If non-nil, Proof General will automatically issue this command +to help speed up processing of long proof scripts. +See also proof-shell-start-silent-cmd. +NOT IMPLEMENTED YET. Forthcoming in next version." + :type '(choice string (const nil)) + :group 'proof-shell) + + ;; ;; 5b. Regexp variables for matching output from proof process. ;; |