src/Pure/General/markup.scala

--- a/src/Pure/General/markup.scala	Fri Apr 01 18:29:10 2011 +0200
+++ b/src/Pure/General/markup.scala	Sun Apr 03 17:35:16 2011 +0200
@@ -97,6 +97,19 @@
   val DEF = "def"
   val REF = "ref"
 
+  object Entity
+  {
+    def unapply(markup: Markup): Option[(String, String)] =
+      markup match {
+        case Markup(ENTITY, props @ Kind(kind)) =>
+          props match {
+            case Name(name) => Some(kind, name)
+            case _ => None
+          }
+        case _ => None
+      }
+  }
+
 
   /* position */