From 4148c1e57a81ea19d4ab8f3f4a271bf08a7dcde3 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 29 Aug 2002 01:38:38 +0000
Subject: Update magic

---
 doc/PG-adapting.texi | 14 +++++++++++---
 1 file 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
 
-- 
cgit v1.2.3