# HG changeset patch
# User wenzelm
# Date 1608121358 -3600
# Node ID 776198313227652b7bdfd170d518beb8191ebb6e
# Parent  25cc8f5184e5527ae4cdfa464d8a357ddd0027ee
tuned signature;

diff -r 25cc8f5184e5 -r 776198313227 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Dec 16 13:17:48 2020 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Dec 16 13:22:38 2020 +0100
@@ -119,7 +119,7 @@
       def unapply(markup: Markup): Option[Long] =
         if (markup.name == ENTITY) Markup.Ref.unapply(markup.properties) else None
     }
-    object Id
+    object Occ
     {
       def unapply(markup: Markup): Option[Long] =
         Def.unapply(markup) orElse Ref.unapply(markup)
diff -r 25cc8f5184e5 -r 776198313227 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Wed Dec 16 13:17:48 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Dec 16 13:22:38 2020 +0100
@@ -453,7 +453,7 @@
                 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.Entity.Id(i), _))) if focus(i) =>
+              case (_, Text.Info(_, XML.Elem(Markup.Entity.Occ(i), _))) if focus(i) =>
                 Some((Nil, Some(Rendering.Color.entity)))
               case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
                 val color =
@@ -542,7 +542,7 @@
     if (focus.defined) {
       snapshot.cumulate[Boolean](defs_range, false, Rendering.entity_elements, _ =>
         {
-          case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) if focus(i) => Some(true)
+          case (_, Text.Info(_, XML.Elem(Markup.Entity.Occ(i), _))) if focus(i) => Some(true)
           case _ => None
         }).flatMap(info => if (info.info) Some(info.range) else None)
     }