From 5c75af0dd3d5341a3e3d93818bf61a015727392e Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Wed, 11 Oct 2006 18:34:26 +0000 Subject: added regexps for begin/end and theory start; --- isar/isar-syntax.el | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'isar/isar-syntax.el') diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 2d657dac..e990c0fe 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -233,7 +233,7 @@ matches contents of quotes for quoted identifiers.") (defconst isar-improper-regexp "\\(\\<[A-Za-z][A-Za-z0-9'_]*_tac\\>\\|\\\\)" - "Regexp matching old-style tactic names") + "Regexp matching low-level features") (defconst isar-save-command-regexp (proof-anchor-regexp (isar-ids-to-regexp isar-keywords-save))) @@ -428,6 +428,18 @@ matches contents of quotes for quoted identifiers.") (defun isar-cannot-undo (cmd) (concat "cannot_undo \"" cmd "\";")) +(defconst isar-theory-start-regexp + (proof-anchor-regexp + (isar-ids-to-regexp + (append isar-keywords-theory-begin + isar-keywords-theory-switch)))) + +(defconst isar-begin-regexp + (isar-ids-to-regexp '("begin"))) ;; no anchor! + +(defconst isar-end-regexp + (proof-anchor-regexp + (isar-ids-to-regexp isar-keywords-theory-end))) (defconst isar-undo-fail-regexp (proof-anchor-regexp -- cgit v1.2.3