# HG changeset patch
# User wenzelm
# Date 1397582870 -7200
# Node ID 5157f7615e99a03794e380db59e9d174d726f2a7
# Parent  1a59587f46ec1e2e85591ab2aff693dfb90ec1d5
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
more robust point_range;
tuned;

diff -r 1a59587f46ec -r 5157f7615e99 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Apr 15 19:11:34 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Apr 15 19:27:50 2014 +0200
@@ -212,7 +212,7 @@
           def pad(range: Text.Range): String =
             if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
 
-          val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
+          val caret = JEdit_Lib.caret_range(text_area)
           val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
           pad(before_caret) + text + pad(caret)
         }
@@ -299,7 +299,7 @@
       spell_checker <- PIDE.spell_checker.get
       doc_view <- PIDE.document_view(text_area)
       rendering = doc_view.get_rendering()
-      range <- JEdit_Lib.before_caret_range(text_area, rendering)
+      range = JEdit_Lib.caret_range(text_area)
       Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
     } {
       spell_checker.update(word, include, permanent)
diff -r 1a59587f46ec -r 5157f7615e99 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 19:11:34 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 19:27:50 2014 +0200
@@ -162,19 +162,21 @@
   /* point range */
 
   def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
-    buffer_lock(buffer) {
-      def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
-      try {
-        val c = text(offset)
-        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
-          Text.Range(offset, offset + 2)
-        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
-          Text.Range(offset - 1, offset + 1)
-        else
-          Text.Range(offset, offset + 1)
+    if (offset < 0) Text.Range.offside
+    else
+      buffer_lock(buffer) {
+        def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
+        try {
+          val c = text(offset)
+          if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
+            Text.Range(offset, offset + 2)
+          else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
+            Text.Range(offset - 1, offset + 1)
+          else
+            Text.Range(offset, offset + 1)
+        }
+        catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
       }
-      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
-    }
 
 
   /* text ranges */
@@ -185,6 +187,9 @@
   def line_range(buffer: JEditBuffer, line: Int): Text.Range =
     Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength)
 
+  def caret_range(text_area: TextArea): Text.Range =
+    point_range(text_area.getBuffer, text_area.getCaretPosition)
+
   def before_caret_range(text_area: TextArea, rendering: Rendering): Option[Text.Range] =
   {
     val range = line_range(text_area.getBuffer, text_area.getCaretLine)
diff -r 1a59587f46ec -r 5157f7615e99 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Apr 15 19:11:34 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Tue Apr 15 19:27:50 2014 +0200
@@ -356,7 +356,7 @@
     val font_context = painter.getFontRenderContext
 
     val caret_range =
-      if (caret_enabled) JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
+      if (caret_enabled) JEdit_Lib.caret_range(text_area)
       else Text.Range.offside
 
     var w = 0.0f