aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2009-10-14 00:52:22 +0000
committerDavid Aspinall2009-10-14 00:52:22 +0000
commit472a463b62d0e834258d081c85e0a353269d4a6b (patch)
treeb1e71f99404f5182b2b9189e44891630f53ed428
parent9f9ed3af6e012b00f66204003548dc91ec06c7c0 (diff)
named entity needed for goal-with-hole
-rw-r--r--isar/isar-syntax.el5
1 files changed, 5 insertions, 0 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index a014337b..61ddf3e9 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -502,6 +502,11 @@ matches contents of quotes for quoted identifiers.")
isar-keywords-theory-script
isar-keywords-theory-goal))
+(defconst isar-named-entity-regexp
+ (concat "\\(" (isar-ids-to-regexp isar-keywords-imenu) "\\)"
+ "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
+ isar-name-regexp "[[:=]" ))
+
(defconst isar-generic-expression
(mapcar (lambda (kw)
(list (capitalize kw)