prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
authorwenzelm
Tue Apr 15 19:27:50 2014 +0200 (2014-04-15)
changeset 565925157f7615e99
parent 56591 1a59587f46ec
child 56593 0ea7c84110ac
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
more robust point_range;
tuned;
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Apr 15 19:11:34 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Apr 15 19:27:50 2014 +0200
     1.3 @@ -212,7 +212,7 @@
     1.4            def pad(range: Text.Range): String =
     1.5              if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
     1.6  
     1.7 -          val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
     1.8 +          val caret = JEdit_Lib.caret_range(text_area)
     1.9            val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
    1.10            pad(before_caret) + text + pad(caret)
    1.11          }
    1.12 @@ -299,7 +299,7 @@
    1.13        spell_checker <- PIDE.spell_checker.get
    1.14        doc_view <- PIDE.document_view(text_area)
    1.15        rendering = doc_view.get_rendering()
    1.16 -      range <- JEdit_Lib.before_caret_range(text_area, rendering)
    1.17 +      range = JEdit_Lib.caret_range(text_area)
    1.18        Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
    1.19      } {
    1.20        spell_checker.update(word, include, permanent)
     2.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 19:11:34 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 19:27:50 2014 +0200
     2.3 @@ -162,19 +162,21 @@
     2.4    /* point range */
     2.5  
     2.6    def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
     2.7 -    buffer_lock(buffer) {
     2.8 -      def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
     2.9 -      try {
    2.10 -        val c = text(offset)
    2.11 -        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
    2.12 -          Text.Range(offset, offset + 2)
    2.13 -        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
    2.14 -          Text.Range(offset - 1, offset + 1)
    2.15 -        else
    2.16 -          Text.Range(offset, offset + 1)
    2.17 +    if (offset < 0) Text.Range.offside
    2.18 +    else
    2.19 +      buffer_lock(buffer) {
    2.20 +        def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
    2.21 +        try {
    2.22 +          val c = text(offset)
    2.23 +          if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
    2.24 +            Text.Range(offset, offset + 2)
    2.25 +          else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
    2.26 +            Text.Range(offset - 1, offset + 1)
    2.27 +          else
    2.28 +            Text.Range(offset, offset + 1)
    2.29 +        }
    2.30 +        catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
    2.31        }
    2.32 -      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
    2.33 -    }
    2.34  
    2.35  
    2.36    /* text ranges */
    2.37 @@ -185,6 +187,9 @@
    2.38    def line_range(buffer: JEditBuffer, line: Int): Text.Range =
    2.39      Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength)
    2.40  
    2.41 +  def caret_range(text_area: TextArea): Text.Range =
    2.42 +    point_range(text_area.getBuffer, text_area.getCaretPosition)
    2.43 +
    2.44    def before_caret_range(text_area: TextArea, rendering: Rendering): Option[Text.Range] =
    2.45    {
    2.46      val range = line_range(text_area.getBuffer, text_area.getCaretLine)
     3.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Apr 15 19:11:34 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Tue Apr 15 19:27:50 2014 +0200
     3.3 @@ -356,7 +356,7 @@
     3.4      val font_context = painter.getFontRenderContext
     3.5  
     3.6      val caret_range =
     3.7 -      if (caret_enabled) JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
     3.8 +      if (caret_enabled) JEdit_Lib.caret_range(text_area)
     3.9        else Text.Range.offside
    3.10  
    3.11      var w = 0.0f