From a4350f7f2d6d194a8387191ed1176414a012daed Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 23 Jan 2011 14:12:58 +0000 Subject: Documentation updates --- doc/PG-adapting.texi | 47 +++++++++++++++++++++++++++++++++-------------- 1 file changed, 33 insertions(+), 14 deletions(-) (limited to 'doc/PG-adapting.texi') diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 7ff873af..5a07cfc5 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -1243,7 +1243,7 @@ switching to B. @c TEXI DOCSTRING MAGIC: proof-no-fully-processed-buffer @defvar proof-no-fully-processed-buffer Set to t if buffers should always retract before scripting elsewhere.@* -Leave at nil if fully processd buffers make sense for the current +Leave at nil if fully processed buffers make sense for the current proof assistant. If nil the user can choose to fully assert a buffer when starting scripting in a different buffer. If t there is only the choice to fully retract the active buffer before @@ -1334,13 +1334,35 @@ to send to the prover to activate certain actions. @c TEXI DOCSTRING MAGIC: proof-prog-name @defvar proof-prog-name System command to run the proof assistant in the proof shell.@* -May contain arguments separated by spaces, but see also @samp{proof-prog-args}. +May contain arguments separated by spaces, but see also the +prover specific settings @samp{-prog-args} and @samp{-prog-env}. -Remark: if @samp{proof-prog-args} is non-nil, then @samp{@code{proof-prog-name}} is considered +Remark: if @samp{-prog-args} is non-nil, then @samp{@code{proof-prog-name}} is considered strictly: it must contain @strong{only} the program name with no option, spaces are interpreted literally as part of the program name. @end defvar +@c TEXI DOCSTRING MAGIC: PA-prog-args +@defvar PA-prog-args +Arguments to be passed to @samp{@code{proof-prog-name}} to run the proof assistant.@* +If non-nil, will be treated as a list of arguments for @samp{@code{proof-prog-name}}. +Otherwise @samp{@code{proof-prog-name}} will be split on spaces to form arguments. + +Remark: Arguments are interpreted strictly: each one must contain only one +word, with no space (unless it is the same word). For example if the +arguments are -x foo -y bar, then the list should be '("-x" "foo" +"-y" "bar"), notice that '("-x foo" "-y bar") is @strong{wrong}. +@end defvar + +@c TEXI DOCSTRING MAGIC: PA-prog-env +@defvar PA-prog-env +Modifications to @samp{@code{process-environment}} made before running @samp{@code{proof-prog-name}}.@* +Each element should be a string of the form ENVVARNAME=@var{value}. They will be +added to the environment before launching the prover (but not pervasively). +For example for coq on Windows you might need something like: +(setq @code{coq-prog-env} '("HOME=C:\Program Files\Coq\")) +@end defvar + @c TEXI DOCSTRING MAGIC: proof-shell-auto-terminate-commands @defvar proof-shell-auto-terminate-commands Non-nil if Proof General should try to add terminator to every command.@* @@ -1385,15 +1407,6 @@ A command for re-initialising the proof process. 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 @samp{@code{proof-shell-quit-cmd}}.@* -After this timeout, the proof shell will be killed off more rudely. -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.@* @@ -3375,11 +3388,17 @@ shell buffer, alled by @samp{@code{proof-shell-bail-out}} if process exits. @end defun @c TEXI DOCSTRING MAGIC: proof-shell-exit -@deffn Command proof-shell-exit +@deffn Command proof-shell-exit &optional dont-ask Query the user and exit the proof process. This simply kills the @samp{@code{proof-shell-buffer}} relying on the hook function -@samp{@code{proof-shell-kill-function}} to do the hard work. + +@samp{@code{proof-shell-kill-function}} to do the hard work. If optional +argument @var{dont-ask} is non-nil, the proof process is terminated +without confirmation. + +The kill function uses @samp{-quit-timeout} as a timeout to wait +after sending @samp{@code{proof-shell-quit-cmd}} before rudely killing the process. @end deffn @c TEXI DOCSTRING MAGIC: proof-shell-bail-out -- cgit v1.2.3