Added proof-shell-auto-terminate-commands

3 files changed, 22 insertions, 3 deletions

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 10b3739a..057eb869 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -901,8 +901,10 @@ a variable which is in the proof assistant's customization
 group.  This allows different proof assistants to coexist
 (albeit in separate Emacs sessions).
 @end defvar
-@c TEXI DOCSTRING MAGIC: proof-shell-pre-sync-init-cmd
 
+@c TEXI DOCSTRING MAGIC: proof-shell-auto-terminate-commands
+
+@c TEXI DOCSTRING MAGIC: proof-shell-pre-sync-init-cmd
 @defvar proof-shell-pre-sync-init-cmd 
 The command for configuring the proof process to gain synchronization.@*
 This command is sent before Proof General's synchronization
@@ -915,6 +917,7 @@ does not need to be set.
 
 See also @samp{@code{proof-shell-init-cmd}}.
 @end defvar
+
 @c TEXI DOCSTRING MAGIC: proof-shell-init-cmd
 @defvar proof-shell-init-cmd 
 The command for initially configuring the proof process.@*
@@ -925,14 +928,17 @@ the proof assistant in some way, or print a welcome message
 
 See also @samp{@code{proof-shell-pre-sync-init-cmd}}.
 @end defvar
+
 @c TEXI DOCSTRING MAGIC: proof-shell-restart-cmd
 @defvar proof-shell-restart-cmd 
 A command for re-initialising the proof process.
 @end defvar
+
 @c TEXI DOCSTRING MAGIC: proof-shell-quit-cmd
 @defvar proof-shell-quit-cmd 
 A command to quit the proof process.  If nil, send EOF instead.
 @end defvar
+
 @c TEXI DOCSTRING MAGIC: proof-shell-quit-timeout
 @defvar proof-shell-quit-timeout 
 The number of seconds to wait after sending @code{proof-shell-quit-cmd}.@*
@@ -941,6 +947,7 @@ If your proof assistant takes a long time to clean up (for
 example writing persistent databases out or the like), you may
 need to bump up this value.
 @end defvar
+
 @c TEXI DOCSTRING MAGIC: proof-shell-cd-cmd
 @defvar proof-shell-cd-cmd 
 Command to the proof assistant to change the working directory.@*
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 4743eac6..758edb5c 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1262,7 +1262,7 @@ See also `proof-shell-init-cmd'."
    :type '(choice string (const nil))
    :group 'proof-shell)
 
-(defcustom proof-shell-init-cmd ""
+(defcustom proof-shell-init-cmd nil
    "The command for initially configuring the proof process.
 This command is sent to the process as soon as syncrhonization is gained
 (when an annotated prompt is first recognized).  It can be used to configure 
@@ -1283,6 +1283,15 @@ See also `proof-shell-pre-sync-init-cmd'."
    :type '(choice string (const nil))
    :group 'proof-shell)
 
+(defcustom proof-shell-auto-terminate-commands t
+  "Non-nil if Proof General should try to add terminator to every command.
+If non-nil, whenever a command is sent to the prover using
+`proof-shell-invisible-command', Proof General will check to see if it
+ends with proof-terminal-char, and add it if not.
+If proof-terminal-char is nil, this has no effect."
+  :type 'boolean
+  :group 'proof-shell)
+
 ;; FIXME could add option to quiz user before rude kill.
 (defcustom proof-shell-quit-timeout 10
   "The number of seconds to wait after sending proof-shell-quit-cmd.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index a63cd8c2..c0d1de04 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1788,12 +1788,15 @@ Calls proof-state-change-hook."
 
 ;;;###autoload
 (defun proof-shell-invisible-command (cmd &optional wait)
-  "Send CMD to the proof process.  Automatically add proof-terminal-char if nec.
+  "Send CMD to the proof process.  
+Automatically add proof-terminal-char if necessary, examining
+proof-shell-no-auto-terminate-commands.
 By default, let the command be processed asynchronously.
 But if optional WAIT command is non-nil, wait for processing to finish
 before and after sending the command.
 If WAIT is an integer, wait for that many seconds afterwards."
   (unless (or (null proof-terminal-char)
+	      (not proof-shell-auto-terminate-commands)
 	      (string-match (concat
 			     (regexp-quote
 			      (char-to-string proof-terminal-char))