diff options
| author | David Aspinall | 2002-08-28 23:06:56 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-08-28 23:06:56 +0000 |
| commit | 78bd1cffbc75c8e56fa3d53eb8bf5751cb38e63c (patch) | |
| tree | 774243b586a7db219662b7d4b89d3006b9e13574 | |
| parent | 1cfaaa8c4e92ccc97234b44372eb3d8c365897fc (diff) | |
Change proof-shell-theorem-dependency-regexp to use two pieces: names and dependencies
| -rw-r--r-- | generic/proof-config.el | 14 | ||||
| -rw-r--r-- | generic/proof-shell.el | 11 |
2 files changed, 19 insertions, 6 deletions
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) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 03c6f29d..ca4e33d7 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1231,9 +1231,14 @@ proof-shell-eager-annotation-start, proof-shell-eager-annotation-end." ;; CASE theorem dependency: prover lists thms used in last proof ((and proof-shell-theorem-dependency-list-regexp (string-match proof-shell-theorem-dependency-list-regexp message)) - (setq proof-last-theorem-dependencies - (split-string (match-string 1 message) - proof-shell-theorem-dependency-list-split))) + (let ((names (match-string 1 message)) + (deps (match-string 2 message))) + (setq proof-last-theorem-dependencies + (cons + (split-string names + proof-shell-theorem-dependency-list-split) + (split-string deps + proof-shell-theorem-dependency-list-split))))) ;; CASE tracing output: output in the tracing buffer instead ;; of the response buffer |