From adb6b5a032dde8a561877cbd0756bf83222ce4d4 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 14 Oct 2009 00:57:37 +0000 Subject: Remove function-menu as promised --- doc/PG-adapting.texi | 70 ++-------------------------------------------------- 1 file changed, 2 insertions(+), 68 deletions(-) (limited to 'doc/PG-adapting.texi') diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 4e406d05..f3876c17 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -810,12 +810,9 @@ it calls @samp{@code{proof-looking-at-syntactic-context}}. @node Recognizing proofs @section Recognizing proofs -Up to three settings each may be supplied for recognizing goal-like and +Several settings each may be supplied for recognizing goal-like and save-like commands. The @code{-with-hole-} settings are used to make a -record of the name of the theorem proved, and also to build a default -value for the rather complicated setting -@code{proof-script-next-entity-regexps}, which activates the @i{function -menu} feature. +record of the name of the theorem proved. The @code{-p} subsidiary predicates were added to allow more discriminating behaviour for particular proof assistants. (This is a @@ -977,70 +974,7 @@ syntax \"word\" syntax during matching." @end defvar -To configure the @i{function menu} feature, there are a couple of -settings. These can be used to recognize named proofs, and other -elements in the proof script as well. -(@b{NOTE}: it is likely that function menu support will be removed -in favour of Imenu only in the next release of Proof General). -@c TEXI DOCSTRING MAGIC: proof-script-next-entity-regexps -@defvar proof-script-next-entity-regexps -Regular expressions to help find definitions and proofs in a script.@* -This is the list of the form -@lisp - (@var{anyentity-regexp} - @var{discriminator-regexp} ... @var{discriminator-regexp}) -@end lisp -The idea is that @var{anyentity-regexp} matches any named entity in the -proof script, on a line where the name appears. This is assumed to be -the start or the end of the entity. The discriminators then test -which kind of entity has been found, to get its name. A -@var{discriminator-regexp} has one of the forms -@lisp - (@var{regexp} @var{matchnos}) - (@var{regexp} @var{matchnos} @code{'backward} @var{backregexp}) - (@var{regexp} @var{matchnos} @code{'forward} @var{forwardregexp}) -@end lisp -If @var{regexp} matches the string captured by @var{anyentity-regexp}, then -@var{matchnos} are the match numbers for the substrings which name the entity -(these may be either a single number or a list of numbers). - -If @code{'backward} @var{backregexp} is present, then the start of the entity -is found by searching backwards for @var{backregexp}. - -Conversely, if @code{'forward} @var{forwardregexp} is found, then the end of -the entity is found by searching forwards for @var{forwardregexp}. - -Otherwise, the start and end of the entity will be the region matched -by @var{anyentity-regexp}. - -This mechanism allows fairly complex parsing of the buffer, in -particular, it allows for goal..save regions which are named -only at the end. However, it does not parse strings, -comments, or parentheses. - -This variable may not need to be set: a default value which should -work for goal..saves is calculated from @samp{@code{proof-goal-with-hole-regexp}}, -@samp{@code{proof-goal-command-regexp}}, and @samp{@code{proof-save-with-hole-regexp}}. -@end defvar - -@c TEXI DOCSTRING MAGIC: proof-script-find-next-entity-fn -@defvar proof-script-find-next-entity-fn -Name of function to find next interesting entity in a script buffer.@* -This is used to configure @code{func-menu}. The default value is -@samp{proof-script-find-next-entity}, which searches for the next entity -based on fume-function-name-regexp which by default is set from -@samp{@code{proof-script-next-entity-regexps}}. - -The function should move point forward in a buffer, and return a cons -cell of the name and the beginning of the entity's region. - -Note that @samp{@code{proof-script-next-entity-regexps}} is set to a default value -from @samp{@code{proof-goal-with-hole-regexp}} and @samp{@code{proof-save-with-hole-regexp}} in -the function @samp{@code{proof-config-done}}, so you may not need to worry about any -of this. See whether function menu does something sensible by -default. -@end defvar @node Configuring undo behaviour @section Configuring undo behaviour -- cgit v1.2.3