diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-08-29 01:38:38 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-29 01:38:38 +0000 |
| commit | 4148c1e57a81ea19d4ab8f3f4a271bf08a7dcde3 (patch) | |
| tree | ce086924cb4b882e07e6dd58e9bc117bc71fa5ad /doc/PG-adapting.texi | |
| parent | 3f0bf7149ad9ad49c7c84566637106485370ef65 (diff) | |
Update magic
Diffstat (limited to 'doc/PG-adapting.texi')
| -rw-r--r-- | doc/PG-adapting.texi | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 9965727c..ca998d1c 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -1764,9 +1764,17 @@ settings. @c TEXI DOCSTRING MAGIC: proof-shell-theorem-dependency-list-regexp @defvar proof-shell-theorem-dependency-list-regexp -Regexp matching output telling Proof General what the dependencies are. @* -This is so that the dependent theorems can be highlighted somehow. -Set to nil to disable. +Regexp matching output telling Proof General about dependencies.@* +This is to allow navigation and display of dependency information. +The output from the prover should be a message with the form +@lisp + @var{dependencies} OF X Y Z ARE A B C +@end lisp +with X Y Z, A B C separated by whitespace or somehow else (see +@samp{@code{proof-shell-theorem-dependency-list-split}}. This variable should +be set to a regexp to match the overall message (which should +be an urgent message), with two sub-matches for X Y Z and A B C. + This is an experimental feature, currently work-in-progress. @end defvar |