Added proof-shell-{start,stop}-silent-cmd.

2 files changed, 22 insertions, 0 deletions

diff --git a/coq/coq.el b/coq/coq.el
index fbd85399..8264fb5a 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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.
 ;;