From d83126ec7b57c1b7f54d8b937925f9b24ae388f0 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 19 Jul 2000 15:47:07 +0000
Subject: changes to add theorem dependencies recording in spans

---
 generic/proof-config.el | 6 +++++-
 generic/proof-script.el | 9 ++++++++-
 generic/proof-shell.el  | 9 +++++++++
 3 files changed, 22 insertions(+), 2 deletions(-)

(limited to 'generic')

diff --git a/generic/proof-config.el b/generic/proof-config.el
index dcd1c32b..cd2b8f8a 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1650,7 +1650,11 @@ to do syntax highlighting with font-lock."
   :type 'boolean
   :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.  Set to nil to disable."
+  :type '(choice nil regexp)
+  :group 'proof-shell)
 
 ;;
 ;; 5c. hooks and other miscellaneous customizations
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 8f4dcace..f3f35bbf 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -33,6 +33,8 @@
 (deflocal proof-active-buffer-fake-minor-mode nil
   "An indication in the modeline that this is the *active* script buffer")
 
+(defvar proof-last-theorem-dependencies nil
+  "Contains the dependencies of the last theorem set in proof-shell-process-urgent-message")
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -156,7 +158,8 @@ buffer, so the regions are made empty by this function."
   (set-span-property proof-locked-span 'end-open t)
   (proof-span-read-only proof-locked-span)
   (set-span-property proof-locked-span 'face 'proof-locked-face)
-  (detach-span proof-locked-span))
+  (detach-span proof-locked-span)
+  (setq proof-last-theorem-dependencies nil))
 
 ;; These two functions are used in coq.el to edit the locked region
 ;; (by lifting local (nested) lemmas out of a proof, to make them global).   
@@ -1013,6 +1016,10 @@ the ACS is marked in the current buffer. If CMD does not match any,
 	(set-span-property gspan 'mouse-face 'highlight)
 	(set-span-property gspan 'type 'goalsave)
 	(set-span-property gspan 'name nam)
+	;; FIONA! New code here:
+	(if proof-last-theorem-dependencies
+	    (set-span-property gspan 'dependencies proof-last-theorem-dependencies))
+	(setq proof-last-theorem-dependencies nil)
 	
 	;; In Coq, we have the invariant that if we've done a save and
 	;; there's a top-level declaration then it must be the
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index c5b11704..bd3aa18c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1400,6 +1400,15 @@ proof-shell-eager-annotation-start, proof-shell-eager-annotation-end."
 	 proof-goals-buffer)
     ;; Erase goals buffer but and possibly its windows
     (proof-clean-buffer proof-goals-buffer))
+   
+   ((if proof-shell-theorem-dependency-list-regexp 
+	(string-match proof-shell-theorem-dependency-list-regexp message))
+      (setq proof-last-theorem-dependencies 
+	  (match-string 1)))
+   
+     ;; FIONA!  New code needs to go in here: match 
+   ;; against proof-shell-theorem-dependency-list-regexp and set a 
+   ;; variable proof-last-theorem-depencies from the match string
 
    (t
     ;; We're about to display a message.  Clear the response buffer
-- 
cgit v1.2.3