From 78bd1cffbc75c8e56fa3d53eb8bf5751cb38e63c Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 28 Aug 2002 23:06:56 +0000
Subject: Change proof-shell-theorem-dependency-regexp to use two pieces: names
 and dependencies

---
 generic/proof-config.el | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'generic/proof-config.el')

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 3f880639..dd72339b 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1959,9 +1959,17 @@ sent when a proof is completed."
   :group 'proof-shell)
 
 (defcustom proof-shell-theorem-dependency-list-regexp nil
-  "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
+
+   DEPENDENCIES OF  X Y Z   ARE  A B C
+
+with X Y Z, A B C separated by whitespace or somehow else (see
+`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."
   :type '(choice nil regexp)
   :group 'proof-shell)
-- 
cgit v1.2.3