--- a/src/Tools/jEdit/src/jedit_rendering.scala Sun Dec 13 16:35:37 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Sun Dec 13 17:48:51 2020 +0100
@@ -225,7 +225,7 @@
/* caret focus */
def entity_ref(range: Text.Range, focus: Rendering.Focus): List[Text.Info[Color]] =
- snapshot.select(range, Rendering.entity_focus_elements, _ =>
+ snapshot.select(range, Rendering.entity_elements, _ =>
{
case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _))
if focus(i) => Some(entity_ref_color)