Download Proof General

Chapter 5: Support for other Packages
33
5.5 Support for tags
An Emacs "tags table" is a description of how a multi-file system is broken up into files. It lists
the names of the component files and the names and positions of the functions (or other named
subunits) in each file. Grouping the related files makes it possible to search or replace through
all the files with one command. Recording the function names and positions makes possible the
M-. command which finds the definition of a function by looking up which of the files it is in.
Some instantiations of Proof General (currently LEGO and Coq) are supplied with external
programs (‘legotags’ and ‘coqtags’) for making tags tables. For example, invoking ‘coqtags
*.v’ produces a file ‘TAGS’ for all files ‘*.v’ in the current directory. Invoking ‘coqtags ‘find .
-name \*.v‘’ produces a file ‘TAGS’ for all files ending in ‘.v’ in the current directory structure.
Once a tag table has been made for your proof developments, you can use the Emacs tags
mechanisms to find tags, and complete symbols from tags table.
One useful key-binding you might want to make is to set the usual tags completion key M-tab to
run tag-complete-symbol to use completion from names in the tag table. To set this binding
in Proof General script buffers, put this code in your ‘.emacs’ file:
(add-hook ’proof-mode-hook
(lambda () (local-set-key ’(meta tab) ’tag-complete-symbol)))
Since this key-binding interferes with a default binding that users may already have customized
(or may be taken by the window manager), Proof General doesn’t do this automatically.
Apart from completion, there are several other operations on tags. One common one is replacing
identifiers across all files using tags-query-replace. For more information on how to use tags,
See Info file ‘(emacs)’, node ‘Tags’.
To use tags for completion at the same time as the completion mechanism mentioned already,
you can use the command M-x add-completions-from-tags-table.
add-completions-from-tags-table
Add completions from the current tags table.
[Command]