Added proof-comment-{start,end}-regexp.

Added proof-segment-up-to-{cmdstart,cmdend} and details of
which is selected.
Updated magic.

1 files changed, 84 insertions, 37 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index abddac3d..beb94d20 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1420,7 +1420,7 @@ Retract the current buffer, and maybe move point to the start.
 @deffn Command proof-electric-terminator-toggle arg
 Toggle @samp{@code{proof-electric-terminator-enable}}. With @var{arg}, turn on iff ARG>0.@*
 This function simply uses @code{customize-set-variable} to set the variable.
-It was constructed with @samp{proof-customize-toggle-fn}.
+It was constructed with @samp{@code{proof-deftoggle-fn}}.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-assert-until-point-interactive
@@ -1510,6 +1510,10 @@ handling of interrupt signals.
 Prompt for a command in the minibuffer and send it to proof assistant.@*
 The command isn't added to the locked region.
 
+If a prefix arg is given and there is a selected region, that is
+pasted into the command.  This is handy for copying terms, etc from
+the script.
+
 If @samp{@code{proof-strict-state-preserving}} is set, and @samp{@code{proof-state-preserving-p}} 
 is configured, then the latter is used as a check that the command
 will be safe to execute, in other words, that it won't ruin
@@ -2132,8 +2136,8 @@ If this table is empty or needs adjusting, please make changes using
 @c TEXI DOCSTRING MAGIC: proof-add-completions
 @deffn Command proof-add-completions 
 Add completions from <PA>-completion-table to completion database.@*
-Uses @samp{@code{add-completion}} with a negative number of uses to discourage
-saving these into the users database.
+Uses @samp{@code{add-completion}} with a negative number of uses and ancient
+last use time, to discourage saving these into the users database.
 @end deffn
 
 The completion facility uses a library @file{completion.el} which
@@ -2591,10 +2595,10 @@ The default value is @code{t}.
 
 @c TEXI DOCSTRING MAGIC: PA-x-symbol-enable
 @defopt PA-x-symbol-enable 
-Whether to use x-symbol in Proof General buffers.@*
-If you activate this variable, whether or not you get x-symbol support
-depends on whether your proof assistant supports it and whether
-X-Symbol is installed in your Emacs.
+Whether to use x-symbol in Proof General for this assistant.@*
+If you activate this variable, whether or not you really get x-symbol
+support depends on whether your proof assistant supports it and
+whether X-Symbol is installed in your Emacs.
 
 The default value is @code{nil}.
 @end defopt
@@ -2671,7 +2675,7 @@ The default value is @code{t}.
 If non-nil, enable indentation code for proof scripts.@*
 Currently the indentation code can be rather slow for large scripts,
 and is critical on the setting of regular expressions for particular
-provers.  Enable it if it works for you.
+provers.  Enable it if it works for you, turn it off if it's too slow.
 
 The default value is @code{nil}.
 @end defopt
@@ -3763,7 +3767,7 @@ script buffer.
 
 @c TEXI DOCSTRING MAGIC: proof-terminal-char
 @defvar proof-terminal-char 
-Character which terminates a command in a script buffer.@*
+Character which terminates a command in a script buffer, or nil if none.@*
 You must set this variable in script mode configuration.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-comment-start
@@ -3776,6 +3780,14 @@ sent to the proof process.
 You should set this variable for reliable working of Proof General,
 as well as @samp{@code{proof-comment-end}}.
 @end defvar
+@c TEXI DOCSTRING MAGIC: proof-comment-start-regexp
+
+@defvar proof-comment-start-regexp 
+Regexp which matches a comment start in the proof command language.
+
+The default value for this is set as (@code{regexp-quote} @code{proof-comment-start})
+but you can set this variable to something else more precise if necessary.
+@end defvar
 @c TEXI DOCSTRING MAGIC: proof-comment-end
 @defvar proof-comment-end 
 String which ends a comment in the proof assistant command language.@*
@@ -3784,11 +3796,22 @@ See also @samp{@code{proof-comment-start}}.
 
 You should set this variable for reliable working of Proof General,
 @end defvar
+
+@c TEXI DOCSTRING MAGIC: proof-comment-end-regexp
+
+
+@defvar proof-comment-end-regexp 
+Regexp which matches a comment end in the proof command language.
+
+The default value for this is set as (@code{regexp-quote} @code{proof-comment-end})
+but you can set this variable to something else more precise if necessary.
+@end defvar
 @c TEXI DOCSTRING MAGIC: proof-case-fold-search
 @defvar proof-case-fold-search 
 Value for @code{case-fold-search} when recognizing portions of proof scripts.@*
-The default value is @code{'nil'}.  If your prover has a case @strong{insensitive}
-input syntax, @code{proof-case-fold-search} should be set to @code{'t'} instead.  
+Also used for completion, via @samp{@code{proof-script-complete}}.
+The default value is @samp{nil}.  If your prover has a case @strong{insensitive}
+input syntax, @code{proof-case-fold-search} should be set to @samp{t} instead.  
 NB: This setting is not used for matching output from the prover.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-save-command-regexp
@@ -4141,13 +4164,11 @@ 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.@*
-The @code{proof-terminal-char} is added on to the end.
+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.@*
-The @code{proof-terminal-char} is added on to the end.
+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 
@@ -4160,9 +4181,9 @@ need to bump up this value.
 @c TEXI DOCSTRING MAGIC: proof-shell-cd-cmd
 @defvar proof-shell-cd-cmd 
 Command to the proof assistant to change the working directory.@*
-The format character @samp{%s} is replaced with the directory, and the
-@code{proof-terminal-char} is added on to the end.  The escape sequences
-in @samp{@code{proof-shell-filename-escapes}} are applied to the filename.
+The format character @samp{%s} is replaced with the directory, and
+the escape sequences in @samp{@code{proof-shell-filename-escapes}} are 
+applied to the filename.
 
 This setting is used to define the function @code{proof-cd} which 
 changes to the value of (@code{default-directory}) for script buffers.
@@ -4918,7 +4939,7 @@ buffer.
 
 @c TEXI DOCSTRING MAGIC: proof-shell-invisible-command
 @defun proof-shell-invisible-command cmd &optional wait
-Send @var{cmd} to the proof process.  Add terminal string if necessary.@*
+Send @var{cmd} to the proof process.  @*
 By default, let the command be processed asynchronously.
 But if optional @var{wait} command is non-nil, wait for processing to finish
 before and after sending the command.
@@ -5087,19 +5108,25 @@ same way as @code{defcustom}, except that the symbol declared will
 automatically be prefixed by the current proof assistant symbol.
 
 @c TEXI DOCSTRING MAGIC: defpgcustom
-@defun defpgcustom 
-Define a new customization variable <PA>-sym for the current proof assistant.@*
+@deffn Macro defpgcustom 
+Define a new customization variable <PA>@var{-sym} for the current proof assistant.@*
 The function proof-assistant-<SYM> is also defined, which can be used in the 
 generic portion of Proof General to set and retrieve the value for the current p.a.
 Arguments as for @samp{defcustom}, which see.
-@end defun
+
+Usage: (defpgcustom SYM &rest @var{args}).
+@end deffn
 In specific instances of Proof General, the macro @code{defpgdefault}
 can be used to give a default value for a generic setting.
 
 @c TEXI DOCSTRING MAGIC: defpgdefault
-@defun defpgdefault 
-Not documented.
-@end defun
+@deffn Macro defpgdefault 
+Set default for the proof assistant specific variable <PA>@var{-sym} to @var{value}.@*
+This should be used in prover-specific code to alter the default values
+for prover specific settings.
+
+Usage: (defpgdefault SYM @var{value})
+@end deffn
 
 All new instantiation variables are best declared using the
 @code{defpgcustom} mechanism (old code may be converted gradually).
@@ -5155,15 +5182,23 @@ Set a customize variable using @code{set-default} and a function.@*
 We first call @samp{@code{set-default}} to set @var{sym} to @var{value}.
 Then if there is a function @var{sym} (i.e. with the same name as the
 variable @var{sym}), it is called to take some dynamic action for the new
-setting.  This only happens when values @strong{change}: we test whether
-proof-config is fully-loaded yet.
+setting.  
+
+If there is no function @var{sym}, we try stripping 
+@code{proof-assistant-symbol} and adding "proof-" instead to get
+a function name.  This extends @code{proof-set-value} to work with
+generic individual settings.
+
+The dynamic action call only happens when values @strong{change}: as an
+approximation we test whether proof-config is fully-loaded yet.
 @end defun
 
 @c TEXI DOCSTRING MAGIC: proof-deftoggle
 @deffn Macro proof-deftoggle 
 Define a function VAR-toggle for toggling a boolean customize setting VAR.@*
-VAR, @var{othername} are not evaluated.  
-The function is defined with @samp{@code{proof-deftoggle-fn}}, which see.
+The toggle function uses @code{customize-set-variable} to change the variable.
+@var{othername} gives an alternative name than the default <VAR>-toggle.
+The name of the defined function is returned.
 @end deffn
 @node Global variables
 @section Global variables
@@ -5367,17 +5402,29 @@ the @code{kill-buffer-hook} for scripting buffers, so that when
 a scripting buffer is killed it is always retracted.
 @end deffn
 
-The next function is the main one used for parsing the proof script
-buffer.
+The function @code{proof-segment-up-to} is the main one used for parsing
+the proof script buffer.  There are several variants of this function
+available corresponding to different parsing strategies; the appropriate
+one is aliased to @code{proof-segment-up-to} according to which
+configuration variables have been set.  If only
+@code{proof-command-end-regexp} or @code{proof-terminal-char} are set,
+then the default is @code{proof-segment-up-to-cmdend}.  If
+@code{proof-command-start-regexp} is set, the choice is
+@code{proof-segment-up-to-cmdstart}.  
+
+@c TEXI DOCSTRING MAGIC: proof-segment-up-to-cmdend
+@defun proof-segment-up-to-cmdend pos &optional next-command-end
+Parse the script buffer from end of locked to @var{pos}.@*
+Return a list of (type, string, int) tuples.
 
-@c TEXI DOCSTRING MAGIC: proof-segment-up-to
-@defun proof-segment-up-to pos &optional next-command-end
-Create a list of (type, int, string) tuples from end of queue/locked region to @var{pos}.@*
 Each tuple denotes the command and the position of its terminator,
 type is one of @code{'comment}, or @code{'cmd}. @code{'unclosed-comment} may be consed onto
 the start if the segment finishes with an unclosed comment.
-If optional @var{next-command-end} is non-nil, we contine past @var{pos} until
-the next command end.
+
+If optional @var{next-command-end} is non-nil, we include the command
+which continues past @var{pos}, if any.
+
+This version is used when @samp{@code{proof-script-command-end-regexp}} is set.
 @end defun
 
 The function @code{proof-semis-to-vanillas} is used to convert
@@ -5388,7 +5435,7 @@ be sent to the proof assistant.
 @defun proof-semis-to-vanillas semis &optional callback-fn
 Convert a sequence of terminator positions to a set of vanilla extents.@*
 Proof terminator positions @var{semis} has the form returned by
-the function @code{proof-segment-up-to}.
+the function proof-segment-up-to.
 Set the callback to @var{callback-fn} or @code{'proof-done-advancing} by default.
 @end defun