diff options
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 |