# HG changeset patch
# User wenzelm
# Date 1393423164 -3600
# Node ID 96ddf9bf12ac8c4933481acaabe19a3fff92293d
# Parent  6a16443e520e880139c34e9824c581023002dc30
more precise before_caret_range (looking both in space and time);

diff -r 6a16443e520e -r 96ddf9bf12ac src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Feb 26 12:15:49 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Feb 26 14:59:24 2014 +0100
@@ -92,6 +92,16 @@
       }
 
 
+    /* caret */
+
+    def before_caret_range(rendering: Rendering): Text.Range =
+    {
+      val snapshot = rendering.snapshot
+      val former_caret = snapshot.revert(text_area.getCaretPosition)
+      snapshot.convert(Text.Range(former_caret - 1, former_caret))
+    }
+
+
     /* rendering */
 
     def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
@@ -100,10 +110,8 @@
         case Some(range) => range.try_restrict(line_range)
         case None =>
           val buffer = text_area.getBuffer
-          val caret = text_area.getCaretPosition
-
-          if (line_range.contains(caret)) {
-            JEdit_Lib.stretch_point_range(buffer, caret).try_restrict(line_range) match {
+          if (line_range.contains(text_area.getCaretPosition)) {
+            before_caret_range(rendering).try_restrict(line_range) match {
               case Some(range) if !range.is_singularity =>
                 rendering.completion_names(range) match {
                   case Some(names) => Some(names.range)
@@ -144,7 +152,7 @@
           val context =
             (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
               case Some(rendering) =>
-                rendering.language_context(JEdit_Lib.stretch_point_range(buffer, caret))
+                rendering.language_context(before_caret_range(rendering))
               case None => None
             }) getOrElse syntax.language_context
 
@@ -182,7 +190,6 @@
       val layered = view.getLayeredPane
       val buffer = text_area.getBuffer
       val painter = text_area.getPainter
-      val caret = text_area.getCaretPosition
 
       val history = PIDE.completion_history.value
       val decode = Isabelle_Encoding.is_active(buffer)
@@ -224,7 +231,7 @@
           PIDE.document_view(text_area) match {
             case Some(doc_view) =>
               val rendering = doc_view.get_rendering()
-              rendering.completion_names(JEdit_Lib.stretch_point_range(buffer, caret)) match {
+              rendering.completion_names(before_caret_range(rendering)) match {
                 case None => None
                 case Some(names) =>
                   JEdit_Lib.try_get_text(buffer, names.range) match {
diff -r 6a16443e520e -r 96ddf9bf12ac src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Feb 26 12:15:49 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Feb 26 14:59:24 2014 +0100
@@ -178,16 +178,6 @@
       catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
     }
 
-  def stretch_point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
-  {
-    val range = point_range(buffer, offset)
-    val left = point_range(buffer, range.start - 1)
-    val right = point_range(buffer, range.stop)
-    val range1 = range.try_join(left) getOrElse range
-    val range2 = range1.try_join(right) getOrElse range1
-    range2
-  }
-
 
   /* visible text range */