From caf7542b618ef6e39853613733c5aa7d4607f224 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 14 Aug 2012 10:37:25 +0000 Subject: Add user option proof-next-command-insert-space. --- doc/ProofGeneral.texi | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) (limited to 'doc/ProofGeneral.texi') diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index f0e074c0..3c3d4a3b 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1501,8 +1501,11 @@ Process the current (or script) buffer, and maybe move point to the end. @end deffn @c TEXI DOCSTRING MAGIC: proof-retract-buffer -@deffn Command proof-retract-buffer -Retract the current buffer, and maybe move point to the start. +@deffn Command proof-retract-buffer &optional called-interactively +Retract the current buffer, and maybe move point to the start.@* +Point is only moved according to @samp{@code{proof-follow-mode}}, if +@var{called-interactively} is non-nil, which is the case for all +interactive calls. @end deffn @c TEXI DOCSTRING MAGIC: proof-electric-terminator-toggle @@ -3457,6 +3460,9 @@ regions of the script. The default value is @code{t}. @end defopt + + + @node User options @section User options @c Index entries for each option 'concept' @@ -3477,7 +3483,7 @@ The default value is @code{t}. @c @cindex formatting proof script Here is a list of the important user options for Proof General, apart from -the three display options mentioned above. +the display options mentioned above. User options can be set via the customization system already mentioned, via the old-fashioned @code{M-x edit-options} mechanism, or simply by @@ -3508,6 +3514,15 @@ terminator somewhere nearby. Electric! The default value is @code{nil}. @end defopt +@c TEXI DOCSTRING MAGIC: proof-next-command-insert-space +@defopt proof-next-command-insert-space +If non-nil, PG will use heuristics to insert newlines or spaces in scripts.@* +In particular, if electric terminator is switched on, spaces or newlines will +be inserted as the user types commands to the prover. + +The default value is @code{t}. +@end defopt + @c TEXI DOCSTRING MAGIC: proof-toolbar-enable @defopt proof-toolbar-enable If non-nil, display Proof General toolbar for script buffers. -- cgit v1.2.3