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