From 472a463b62d0e834258d081c85e0a353269d4a6b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 14 Oct 2009 00:52:22 +0000
Subject: named entity needed for goal-with-hole

---
 isar/isar-syntax.el | 5 +++++
 1 file changed, 5 insertions(+)

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)
-- 
cgit v1.2.3