From 2cd8b2cd5cb166c46a1b76cd527d1b98d778ec9e Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Thu, 5 May 2011 09:18:23 +0000 Subject: - flushed proof-done-advancing-require-function and proof-shell-require-command-regexp - TAGS updated to really flush them --- doc/PG-adapting.texi | 15 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) (limited to 'doc') diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index c526d2df..27dcb0df 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -1918,22 +1918,9 @@ be set non-nil, so that when a completed file is activated for scripting (to do undo operations), the whole history is discarded. @end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-require-command-regexp -@defvar proof-shell-require-command-regexp -A regular expression to match a Require-type of command, or nil.@* -If set to a regexp, then @samp{@code{proof-done-advancing-require-function}} -should also be set, and will be called immediately after the match. -This can be used to adjust @samp{@code{proof-included-files-list}} based on the -lines of script that have been processed/parsed, rather than relying -on information from the prover. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-done-advancing-require-function -@defvar proof-done-advancing-require-function -Used in @samp{@code{proof-done-advancing}}, see @samp{@code{proof-shell-require-command-regexp}}.@* -The function is passed the span and the command as arguments. -@end defvar + @node Hooks and other settings @section Hooks and other settings -- cgit v1.2.3