# HG changeset patch
# User wenzelm
# Date 1347897370 -7200
# Node ID 215ba6884bdf3ee2c8b583a8f650e5b1246a9cbb
# Parent  38db4832b210259669df4d6fbe26df2d6b47e712
tuned signature;

diff -r 38db4832b210 -r 215ba6884bdf src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Sep 17 17:49:11 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Sep 17 17:56:10 2012 +0200
@@ -92,24 +92,6 @@
   }
 
 
-
-  /* point range */
-
-  def point_range(offset: Text.Offset): Text.Range =
-    JEdit_Lib.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) }
-    }
-
-
   /* pending text edits */
 
   private object pending_edits  // owned by Swing thread
diff -r 38db4832b210 -r 215ba6884bdf src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Mon Sep 17 17:49:11 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Sep 17 17:56:10 2012 +0200
@@ -204,7 +204,8 @@
       if (control && model.buffer.isLoaded) {
         JEdit_Lib.buffer_lock(model.buffer) {
           val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
-          val mouse_range = model.point_range(text_area.xyToOffset(e.getX(), e.getY()))
+          val mouse_range =
+            JEdit_Lib.point_range(model.buffer, text_area.xyToOffset(e.getX(), e.getY()))
           active_areas.foreach(_.update_rendering(rendering, mouse_range))
         }
       }
diff -r 38db4832b210 -r 215ba6884bdf src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Sep 17 17:49:11 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Sep 17 17:56:10 2012 +0200
@@ -60,5 +60,22 @@
     try { buffer.readLock(); body }
     finally { buffer.readUnlock() }
   }
+
+
+  /* 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)
+      }
+      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
+    }
 }
 
diff -r 38db4832b210 -r 215ba6884bdf src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Mon Sep 17 17:49:11 2012 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Mon Sep 17 17:56:10 2012 +0200
@@ -185,7 +185,8 @@
           else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
 
         val caret_range =
-          if (text_area.isCaretVisible) model.point_range(text_area.getCaretPosition)
+          if (text_area.isCaretVisible)
+            JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
           else Text.Range(-1)
 
         val markup =