aboutsummaryrefslogtreecommitdiffhomepage
path: root/isa
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-29 01:35:23 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-29 01:35:23 +0000
commit2e16755e3b5a6a2ecbc9cb492784d5e0b00a740d (patch)
treed87e3a5013877570dea078a6a35e95efb5032fc3 /isa
parenta06bdccabcaf4878ebf6353eecd3a5f1c980f1bd (diff)
New theorem deps settings
Diffstat (limited to 'isa')
-rw-r--r--isa/isa.el7
1 files changed, 5 insertions, 2 deletions
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