# HG changeset patch
# User wenzelm
# Date 1607895030 -3600
# Node ID 8f586c24107100ac652ff1d07f670da4fa8e9d7c
# Parent  3c09adb4b04249336b061df07a1609eeefda45c9
tuned signature;

diff -r 3c09adb4b042 -r 8f586c241071 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) =>
diff -r 3c09adb4b042 -r 8f586c241071 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Dec 13 19:04:46 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Dec 13 22:30:30 2020 +0100
@@ -445,12 +445,8 @@
                 Some((Nil, Some(Rendering.Color.bad)))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
                 Some((Nil, Some(Rendering.Color.intensify)))
-              case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
-                props match {
-                  case Markup.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
-                  case Markup.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
-                  case _ => None
-                }
+              case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) if focus(i) =>
+                Some((Nil, Some(Rendering.Color.entity)))
               case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
                 val color =
                   depth % 4 match {
@@ -534,12 +530,8 @@
       val results =
         snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_elements, _ =>
           {
-            case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
-              props match {
-                case Markup.Def(i) if focus(i) => Some(true)
-                case Markup.Ref(i) if focus(i) => Some(true)
-                case _ => None
-              }
+            case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) if focus(i) => Some(true)
+            case _ => None
           })
       for (info <- results if info.info) yield info.range
     }