src/Tools/jEdit/src/jedit_rendering.scala
changeset 72901 16fd39c9e31f
parent 72900 c9813630cca4
child 72902 3c09adb4b042
equal deleted inserted replaced
72900:c9813630cca4 72901:16fd39c9e31f
   223 
   223 
   224 
   224 
   225   /* caret focus */
   225   /* caret focus */
   226 
   226 
   227   def entity_ref(range: Text.Range, focus: Rendering.Focus): List[Text.Info[Color]] =
   227   def entity_ref(range: Text.Range, focus: Rendering.Focus): List[Text.Info[Color]] =
   228     snapshot.select(range, Rendering.entity_focus_elements, _ =>
   228     snapshot.select(range, Rendering.entity_elements, _ =>
   229       {
   229       {
   230         case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _))
   230         case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _))
   231         if focus(i) => Some(entity_ref_color)
   231         if focus(i) => Some(entity_ref_color)
   232         case _ => None
   232         case _ => None
   233       })
   233       })