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-shell.el | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'generic/proof-shell.el') 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 -- cgit v1.2.3