From 2e16755e3b5a6a2ecbc9cb492784d5e0b00a740d Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 29 Aug 2002 01:35:23 +0000 Subject: New theorem deps settings --- isa/isa.el | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'isa') diff --git a/isa/isa.el b/isa/isa.el index 387a3ce0..e133b2bf 100644 --- a/isa/isa.el +++ b/isa/isa.el @@ -204,8 +204,11 @@ and script mode." proof-shell-clear-response-regexp "Proof General, please clear the response buffer." proof-shell-clear-goals-regexp "Proof General, please clear the goals buffer." proof-shell-set-elisp-variable-regexp "Proof General, please set the variable \\([^ ]+\\) to: #\\([^#]+\\)#\\." - proof-shell-theorem-dependency-list-regexp "Proof General, theorem dependencies are: \\(.*\\)" - proof-shell-show-dependency-cmd "thm \"%s\";" + + ;; Theorem dependencies. NB: next regex anchored at end with eager annot end + proof-shell-theorem-dependency-list-regexp "Proof General, theorem dependencies of \\(.*\\) are \"\\(.*\\)\"\361" + proof-shell-theorem-dependency-list-split "\" \"" + proof-shell-show-dependency-cmd "thm %s;" ;; Dirty hack to allow font-locking for output based on hidden ;; annotations, see isa-output-font-lock-keywords-1 -- cgit v1.2.3