src/Tools/jEdit/src/isabelle.scala
changeset 73168 25cc8f5184e5
parent 73167 69f768aff611
child 73170 0cc298e29aff
equal deleted inserted replaced
73167:69f768aff611 73168:25cc8f5184e5
   357   def select_entity(text_area: JEditTextArea)
   357   def select_entity(text_area: JEditTextArea)
   358   {
   358   {
   359     for (doc_view <- Document_View.get(text_area)) {
   359     for (doc_view <- Document_View.get(text_area)) {
   360       val rendering = doc_view.get_rendering()
   360       val rendering = doc_view.get_rendering()
   361       val caret_range = JEdit_Lib.caret_range(text_area)
   361       val caret_range = JEdit_Lib.caret_range(text_area)
   362       val active_focus = rendering.caret_focus_ranges(caret_range, Text.Range.full)
   362       val buffer_range = JEdit_Lib.buffer_range(text_area.getBuffer)
       
   363       val active_focus = rendering.caret_focus_ranges(caret_range, buffer_range)
   363       if (active_focus.nonEmpty) {
   364       if (active_focus.nonEmpty) {
   364         text_area.selectNone()
   365         text_area.selectNone()
   365         for (r <- active_focus)
   366         for (r <- active_focus)
   366           text_area.addToSelection(new Selection.Range(r.start, r.stop))
   367           text_area.addToSelection(new Selection.Range(r.start, r.stop))
   367       }
   368       }