--- a/src/Tools/jEdit/src/jedit_rendering.scala Sun Dec 13 16:00:52 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Sun Dec 13 16:35:37 2020 +0100
@@ -224,11 +224,11 @@
/* caret focus */
- def entity_ref(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
- snapshot.select(range, Rendering.caret_focus_elements, _ =>
+ def entity_ref(range: Text.Range, focus: Rendering.Focus): List[Text.Info[Color]] =
+ snapshot.select(range, Rendering.entity_focus_elements, _ =>
{
- case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _)) if focus(i) =>
- Some(entity_ref_color)
+ case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _))
+ if focus(i) => Some(entity_ref_color)
case _ => None
})