src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Sun Dec 13 19:04:46 2020 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Dec 13 22:30:30 2020 +0100
@@ -109,6 +109,22 @@
 
   object Entity
   {
+    object Def
+    {
+      def unapply(markup: Markup): Option[Long] =
+        if (markup.name == ENTITY) Markup.Def.unapply(markup.properties) else None
+    }
+    object Ref
+    {
+      def unapply(markup: Markup): Option[Long] =
+        if (markup.name == ENTITY) Markup.Ref.unapply(markup.properties) else None
+    }
+    object Id
+    {
+      def unapply(markup: Markup): Option[Long] =
+        Def.unapply(markup) orElse Ref.unapply(markup)
+    }
+
     def unapply(markup: Markup): Option[(String, String)] =
       markup match {
         case Markup(ENTITY, props) =>