diff options
| author | Makarius Wenzel | 1999-07-02 22:14:21 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 1999-07-02 22:14:21 +0000 |
| commit | ed7765512723aff20633956d5f8769670fc223c4 (patch) | |
| tree | 9f954d266adffd4aaa45e75b26794840b656e161 | |
| parent | 9af3b0e0bca207591b8172bc859c529edeea32cf (diff) | |
fixed some regexps via proof-anchor-regexp;
| -rw-r--r-- | isar/isar-syntax.el | 6 | ||||
| -rw-r--r-- | isar/isar.el | 7 |
2 files changed, 7 insertions, 6 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 64eb05ae..1cf6a5d2 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -108,15 +108,15 @@ "*Font-lock table for Isabelle terms.") (defconst isar-save-command-regexp - (concat "^" (proof-ids-to-regexp isar-keywords-save))) + (proof-anchor-regexp (proof-ids-to-regexp isar-keywords-save))) (defconst isar-save-with-hole-regexp "$^") ; n.a. (defconst isar-goal-command-regexp - (proof-ids-to-regexp isar-keywords-theory-goal)) + (proof-anchor-regexp (proof-ids-to-regexp isar-keywords-theory-goal))) (defconst isar-local-goal-command-regexp - (proof-ids-to-regexp isar-keywords-proof-goal)) + (proof-anchor-regexp (proof-ids-to-regexp isar-keywords-proof-goal))) (defconst isar-goal-with-hole-regexp (concat "\\(" (proof-ids-to-regexp isar-keywords-theory-goal) "\\)" isar-name-regexp ":") diff --git a/isar/isar.el b/isar/isar.el index e42c5bd2..6b39686e 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -443,13 +443,14 @@ Resulting output from Isabelle will be parsed by Proof General." (defconst isar-undo-fail-regexp - (proof-ids-to-regexp (append isar-keywords-control isar-keywords-theory-end))) + (proof-anchor-regexp + (proof-ids-to-regexp (append isar-keywords-control isar-keywords-theory-end)))) (defconst isar-undo-skip-regexp - (proof-ids-to-regexp isar-keywords-diag)) + (proof-anchor-regexp (proof-ids-to-regexp isar-keywords-diag))) (defconst isar-undo-kill-regexp - (proof-ids-to-regexp isar-keywords-theory-begin)) + (proof-anchor-regexp (proof-ids-to-regexp isar-keywords-theory-begin))) ;; undo proof commands |