Explain how to configure Imenu.

1 files changed, 90 insertions, 17 deletions

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 55eaf6e2..621069d7 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -376,7 +376,7 @@ directory and elisp file for the mode, which will be
 where @samp{PROOF-HOME-DIRECTORY} is the value of the
 variable @code{proof-home-directory}.
 
-The default value is @code{((demoisa "Isabelle Demo" "\\.ML$") (isa "Isabelle" "\\.ML$\\|\\.thy$") (isar "Isabelle/Isar" "\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$\\|\\.v8$\\|\\.v7$") (phox "PhoX" "\\.phx$") (hol98 "HOL" "\\.sml$") (acl2 "ACL2" "\\.acl2$") (twelf "Twelf" "\\.elf$") (plastic "Plastic" "\\.lf$") (lclam "Lambda-CLAM" "\\.lcm$"))}.
+The default value is @code{((demoisa "Isabelle Demo" "\\.ML$") (isa "Isabelle" "\\.ML$\\|\\.thy$") (isar "Isabelle/Isar" "\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$\\|\\.v8$\\|\\.v7$") (phox "PhoX" "\\.phx$") (ccc "CASL Consistency Checker" "\\.ccc$") (hol98 "HOL" "\\.sml$") (acl2 "ACL2" "\\.acl2$") (twelf "Twelf" "\\.elf$") (plastic "Plastic" "\\.lf$") (lclam "Lambda-CLAM" "\\.lcm$") (pgshell "PG-Shell" "\\.pgsh$"))}.
 @end defopt
 
 
@@ -793,10 +793,13 @@ but you can set this variable to something else more precise if necessary.
 @c TEXI DOCSTRING MAGIC: proof-script-comment-end
 @defvar proof-script-comment-end 
 String which ends a comment in the proof assistant command language.@*
-The script buffer's @code{comment-end} is set to a space plus this string.
+Should be an empty string if comments are terminated by @code{end-of-line}
+The script buffer's @code{comment-end} is set to a space plus this string,
+if it is non-empty.
+
 See also @samp{@code{proof-script-comment-start}}.
 
-You should set this variable for reliable working of Proof General,
+You should set this variable for reliable working of Proof General.
 @end defvar
 
 @c TEXI DOCSTRING MAGIC: proof-script-comment-end-regexp
@@ -843,18 +846,6 @@ of an atomic undo block, and (2) to construct the default
 for @samp{@code{proof-script-next-entity-regexps}} used for function menus.
 @end defvar
 
-@c TEXI DOCSTRING MAGIC: proof-goal-with-hole-regexp
-@defvar proof-goal-with-hole-regexp 
-Regexp which matches a command used to issue and name a goal.@*
-The name of the theorem is build from the variable
-@code{proof-goal-with-hole-result} using the same convention as 
-@code{query-replace-regexp}. 
-Used for setting names of goal..save regions and for default
-@code{function-menu} configuration in @code{proof-script-find-next-entity}.
-
-It's safe to leave this setting as nil.
-@end defvar
-
 @c TEXI DOCSTRING MAGIC: proof-goal-command-p
 @defvar proof-goal-command-p 
 A function to test: is this really a goal command?
@@ -866,6 +857,28 @@ look like definitions, etc.  (In the future we may generalize
 @end defvar
 
 
+@c TEXI DOCSTRING MAGIC: proof-goal-with-hole-regexp
+@defvar proof-goal-with-hole-regexp 
+Regexp which matches a command used to issue and name a goal.@*
+The name of the theorem is built from the variable
+@code{proof-goal-with-hole-result} using the same convention as 
+for @samp{@code{query-replace-regexp}}. 
+Used for setting names of goal..save regions and for default
+configuration of other modes (function menu, imenu).
+
+It's safe to leave this setting as nil.
+@end defvar
+
+@c TEXI DOCSTRING MAGIC: proof-goal-with-hole-result
+
+
+@defvar proof-goal-with-hole-result 
+String or Int: how to build the theorem name after matching@*
+with @code{proof-goal-with-hole-regexp}. If it is an int N use @code{match-string} 
+to recover the value of the Nth parenthesis matched. If it is a string
+use @code{replace-match}. It the later case, @code{proof-goal-with-hole-regexp} should
+match the entire command
+@end defvar
 @c TEXI DOCSTRING MAGIC: proof-save-command-regexp
 @defvar proof-save-command-regexp 
 Matches a save command.
@@ -922,10 +935,70 @@ proofs smoothly.
 
 @node Recognizing other elements
 @section Recognizing other elements
+@vindex proof-goal-with-hole-regexp
+@vindex proof-goal-with-hole-result
+
+To configure @i{Imenu} (which in turn configures @i{Speedbar}), 
+you may use the following setting.  If this is unset, a generic
+setting based on @code{proof-goal-with-hole-regexp} is configured.
+
+@c TEXI DOCSTRING MAGIC: proof-script-imenu-generic-expression
+@defvar proof-script-imenu-generic-expression 
+Regular expressions to help find definitions and proofs in a script.@*
+Value for @samp{@code{imenu-generic-expression}}, see documentation of Imenu
+and that variable for details.
+@end defvar
+
+@c This is _not_ docstring magic, but docstring-by-hand from 
+@c imenu.el in XEmacs 21.4.12
+@defvar imenu-generic-expression
+The regex pattern to use for creating a buffer index.
+
+If non-nil this pattern is passed to @samp{imenu--generic-function}
+to create a buffer index.
+
+The value should be an alist with elements that look like this:
+@lisp
+ (@var{menu-title} @var{regexp} @var{index})
+@end lisp
+or like this:
+@lisp
+ (@var{menu-title} @var{regexp} @var{index} @var{function} ARGUMENTS...)
+@end lisp
+with zero or more ARGUMENTS.  The former format creates a simple element in
+the index alist when it matches; the latter creates a special element
+of the form  (@var{name} @var{function} @var{position-marker} ARGUMENTS...)
+with @var{function} and @var{arguments} beiong copied from @samp{imenu-generic-expression}.
+
+@var{menu-title} is a string used as the title for the submenu or nil if the
+entries are not nested.
+
+@var{regexp} is a regexp that should match a construct in the buffer that is
+to be displayed in the menu; i.e., function or variable definitions,
+etc.  It contains a substring which is the name to appear in the
+menu.  See the info section on Regexps for more information.
+
+@var{index} points to the substring in @var{regexp} that contains the name (of the
+function, variable or type) that is to appear in the menu.
+
+The variable is buffer-local.
+
+The variable @samp{imenu-case-fold-search} determines whether or not the
+regexp matches are case sensitive. and @samp{imenu-syntax-alist} can be
+used to alter the syntax table for the search.
+
+For example, see the value of @samp{lisp-imenu-generic-expression} used by
+@samp{lisp-mode} and @samp{emacs-lisp-mode} with @samp{imenu-syntax-alist} set
+locally to give the characters which normally have \"punctuation\"
+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.
+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 
@@ -2613,7 +2686,7 @@ in the @code{proof-assistants} setting.
 @c TEXI DOCSTRING MAGIC: proof-assistants
 @defopt proof-assistants 
 Choice of proof assistants to use with Proof General.@*
-A list of symbols chosen from: @code{'demoisa} @code{'isa} @code{'isar} @code{'lego} @code{'coq} @code{'phox} @code{'hol98} @code{'acl2} @code{'twelf} @code{'plastic} @code{'lclam}.
+A list of symbols chosen from: @code{'demoisa} @code{'isa} @code{'isar} @code{'lego} @code{'coq} @code{'phox} @code{'ccc} @code{'hol98} @code{'acl2} @code{'twelf} @code{'plastic} @code{'lclam} @code{'pgshell}.
 If nil, the default will be ALL proof assistants.
 
 Each proof assistant defines its own instance of Proof General,