diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 6 | ||||
| -rw-r--r-- | generic/proof-script.el | 9 | ||||
| -rw-r--r-- | generic/proof-shell.el | 9 |
3 files changed, 22 insertions, 2 deletions
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 |