Added proof-rsh-command to help complete documentation (was allocated

to tms but he said he wouldn't get around to it)

4 files changed, 66 insertions, 39 deletions

diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi
index 7f5a8c4d..a8c18e31 100644
--- a/doc/NewDoc.texi
+++ b/doc/NewDoc.texi
@@ -794,7 +794,9 @@ For more help, see @inforef{Easy Customization, ,xemacs}.
 @cindex{Toolbar follow mode}
 @cindex{Toolbar disabling}
 @cindex{Proof script indentation}
-@cindex{indentation}
+@cindex{Indentation}
+@cindex{Remote shell}
+@cindex{Running proof assistant remotely}
 @c @cindex{formatting proof script}
 
 
@@ -890,19 +892,25 @@ The configuration settings appear in the customization group
     Proof-General -> Internals ->  Prover Config
 @end lisp
 
-Some examples of settings you may like to tweak are:
+One basic example of a setting you may like to tweak is:
 
-proof-assistant-home-page
+@defvar proof-assistant-home-page
+Web address for information on proof assistant.
+@end var
 
-
-More details of the settings are given in @xref{Adapting Proof General
-to New Provers}.
+Most of the others are more complicated.  More details of the settings
+are given in @xref{Adapting Proof General to New Provers}.  To browse
+them, you can look through the customization groups
+@code{prover-config}, @code{proof-script} and @code{proof-shell}.  The
+group @code{proof-script} contains the configuration variables for
+scripting, and the group @code{proof-shell} contains those for
+interacting with the proof assistant.
 
 Unfortunately, although you can use the customization mechanism to set
 and save these variables, saving them may have no effect because the
-default settings are mostly hard-wired into the proof assistant code.
-@c FIXME: this is a problem, code does need fixing.
-At present there is no easy way to get around this.
+default settings are often hard-wired into the proof assistant code.  At
+present there is no easy way to get around this other than by editing
+the source code.  Please contact us if this proves to be a problem.
 
 
 @node LEGO Proof General
diff --git a/generic/proof-config.el b/generic/proof-config.el
index c047f342..5a5bc089 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -64,11 +64,6 @@
   :type 'boolean
   :group 'proof-general)
 
-(defcustom proof-one-command-per-line nil
-  "*If non-nil, format for newlines after each proof command in a script."
-  :type 'boolean
-  :group 'proof-general)
-
 (and (featurep 'toolbar)
 (defcustom proof-toolbar-wanted t
   "*Whether to use toolbar in proof mode."
@@ -112,11 +107,32 @@ you a reprimand!)"
   ;; confident about it.  (I don't). -da
   "If non-nil, enable indentation code for proof scripts.
 Currently the indentation code can be rather slow for large scripts,
-or may be critical on the setting of regular expressions for 
-particular provers."
+and is critical on the setting of regular expressions for particular
+provers.  Enable it if it works for you."  
+  :type 'boolean 
+  :group 'proof-general)
+
+(defcustom proof-one-command-per-line nil
+  "*If non-nil, format for newlines after each proof command in a script.
+This option is not fully-functional at the moment."
   :type 'boolean
   :group 'proof-general)
 
+(defcustom proof-rsh-command ""
+  "Shell command prefix to run a command on a remote host.  
+For example,
+
+   ssh bigjobs
+
+Would cause Proof General to issue the command 'ssh bigjobs isabelle'
+to start Isabelle remotely on our large compute server called 'bigjobs'.
+
+The protocol used should be configured so that no user interaction
+(passwords, or whatever) is required to get going."
+  :type 'string
+  :group 'proof-general)
+
+
 ;;
 ;; Faces.
 ;; We ought to test that these work sensibly:
@@ -424,25 +440,27 @@ to `nil' of the proof assistant does not support nested goals."
   :type 'function
   :group 'proof-script)
 
-(defcustom proof-atomic-sequence-lists nil
-  "list of instructions for setting up atomic sequences of commands (ACS).
-
-Each instruction is
-a list of the form `(END START &optional FORGET-COMMAND)'. END is a
-regular expression to recognise the last command in an ACS. START
-is a function. Its input is the last command of an ACS. Its output
-is a regular exression to recognise the first command of the ACS.
-It is evaluated once and the output is successively matched agains
-previously processed commands until a match occurs (or the
-beginning of the current buffer is reached). The region determined
-by (START,END) is locked as an ACS. Optionally, the ACS is
-annotated with the actual command to retract the ACS. This is
-computed by applying FORGET-COMMAND to the first and last command
-of the ACS."
-  ;; FIXME customize broken on choices with function in them?
-  ;;:type '(repeat (cons regexp function (choice (const nil) function)))
-  :type '(repeat (cons regexp function function))
-  :group 'proof-shell)
+; Not yet implemented.
+;
+;(defcustom proof-atomic-sequence-lists nil
+;  "list of instructions for setting up atomic sequences of commands (ACS).
+
+;Each instruction is
+;a list of the form `(END START &optional FORGET-COMMAND)'. END is a
+;regular expression to recognise the last command in an ACS. START
+;is a function. Its input is the last command of an ACS. Its output
+;is a regular exression to recognise the first command of the ACS.
+;It is evaluated once and the output is successively matched agains
+;previously processed commands until a match occurs (or the
+;beginning of the current buffer is reached). The region determined
+;by (START,END) is locked as an ACS. Optionally, the ACS is
+;annotated with the actual command to retract the ACS. This is
+;computed by applying FORGET-COMMAND to the first and last command
+;of the ACS."
+;  ;; FIXME customize broken on choices with function in them?
+;  ;;:type '(repeat (cons regexp function (choice (const nil) function)))
+;  :type '(repeat (cons regexp function function))
+;  :group 'proof-shell)
 
 
 (defconst proof-no-command "COMMENT"
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index d3bc5bc0..78e60a7c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -192,7 +192,11 @@ Does nothing if proof assistant is already running."
       (message (format "Starting %s process..." proc))
 
       ;; Starting the inferior process (asynchronous)
-      (let ((prog-name-list (proof-string-to-list proof-prog-name " ")))
+      (let ((prog-name-list (proof-string-to-list 
+			     (concat 
+			      proof-rsh-command
+			      " "
+			      proof-prog-name) " ")))
 	(apply 'make-comint  (append (list proc (car prog-name-list) nil)
 				     (cdr prog-name-list))))
       ;; To send any initialisation commands to the inferior process,
diff --git a/todo b/todo
index 2646ce38..0a8c3076 100644
--- a/todo
+++ b/todo
@@ -149,9 +149,6 @@ C proof-find-next-terminator doesn't work properly:
      bug. Perhaps just use new implementation of
      proof-assert-until-point (30min)
 
-B Add proof-rsh-command and note in documentation about how to
-  use widely-advertised "remote shell" feature.  (1hr tms)
-
 B Add proof-quit-command: some provers may like a quit command to be
   sent to the shell, not just EOF !  (see proof-stop-shell).
   Also reconcile proof-restart-script and proof-stop-shell, see