diff options
Diffstat (limited to 'generic/proof-config.el')
-rw-r--r-- | generic/proof-config.el | 31 |
1 files changed, 26 insertions, 5 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index c52421ae..54c6e6fb 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -556,7 +556,8 @@ information about what Proof General is doing." (defcustom proof-terminal-char nil - "Character which terminates a command in a script buffer." + "Character which terminates a command in a script buffer. +You must set this variable." :type 'character :group 'proof-script) @@ -854,22 +855,42 @@ group. This allows different proof assistants to coexist :group 'proof-shell) (defcustom proof-shell-init-cmd "" - "The command for initially configuring the proof process." + "The command for initially configuring the proof process. +This command is sent to the process as soon as it starts up, +perhaps in order to configure it for Proof General or to +print a welcome message. +Note that it is sent before Proof General's synchronization +mechanism is engaged (in case the command engages it). It +is better to configure the proof assistant via command +line options is possible." :type '(choice string (const nil)) :group 'proof-shell) (defcustom proof-shell-restart-cmd "" - "A command for re-initialising the proof process." + "A command for re-initialising the proof process. +The proof-terminal-char is added on to the end." :type '(choice string (const nil)) :group 'proof-shell) (defcustom proof-shell-quit-cmd nil - "A command to quit the proof process. If nil, send EOF instead." + "A command to quit the proof process. If nil, send EOF instead. +The proof-terminal-char is added on to the end." :type '(choice string (const nil)) :group 'proof-shell) (defcustom proof-shell-cd nil - "Command to the proof assistant to change the working directory." + "Command to the proof assistant to change the working directory. +The format character %s is replaced with the directory, and the +proof-terminal-char is added on to the end. + +This is used to define the function proof-cd which +changes to the value of (default-directory) for script buffers. +For files, the value of (default-directory) is simply the +directory the file resides in. + +NB: By default, proof-cd is called from proof-activate-scripting-hook, +so that the prover switches to the directory of a proof +script everytime scripting begins." :type 'string :group 'proof-shell) |