# 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) }