diff options
| -rw-r--r-- | isa/isa.el | 7 | ||||
| -rw-r--r-- | isar/isar.el | 6 |
2 files changed, 10 insertions, 3 deletions
@@ -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 |