New theorem deps settings

2 files changed, 10 insertions, 3 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
diff --git a/isar/isar.el b/isar/isar.el
index 5bd8bcef..9b6581f4 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -230,7 +230,11 @@ See -k option for Isabelle interface script."
    ;; Some messages delimited by eager annotations
    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-theorem-dependency-list-regexp "Proof General, theorem dependencies are: \\(.*\\)"
+
+   ;; 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;"
 
    ;; Allow font-locking for output based on hidden annotations, see
    ;; isar-output-font-lock-keywords-1