src/Tools/jEdit/src/jedit_rendering.scala
changeset 72901 16fd39c9e31f
parent 72900 c9813630cca4
child 72902 3c09adb4b042
--- 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)