clarified stretch_point_range wrt. UTF-16 surrogates;
authorwenzelm
Sun, 23 Feb 2014 16:08:38 +0100
changeset 55690 d73949233c2e
parent 55689 13b58baf994b
child 55691 aeba7cd45400
clarified stretch_point_range wrt. UTF-16 surrogates; tuned;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Sun Feb 23 15:38:21 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Sun Feb 23 16:08:38 2014 +0100
@@ -115,7 +115,9 @@
             val context =
               (PIDE.document_view(text_area) match {
                 case None => None
-                case Some(doc_view) => doc_view.get_rendering().completion_context(caret)
+                case Some(doc_view) =>
+                  val rendering = doc_view.get_rendering()
+                  rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret))
               }) getOrElse syntax.completion_context
 
             syntax.completion.complete(history, decode, explicit, text, context) match {
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Feb 23 15:38:21 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Feb 23 16:08:38 2014 +0100
@@ -177,6 +177,16 @@
       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 */
 
--- a/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 15:38:21 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 16:08:38 2014 +0100
@@ -273,41 +273,27 @@
 
   /* completion */
 
-  def completion_range(caret: Text.Offset): Option[Text.Range] =
-    if (!snapshot.is_outdated) {
-      snapshot.select(Text.Range(caret - 1, caret + 1), Rendering.completion_names_elements, _ =>
-        {
-          case Completion.Names.Info(names) => Some(names.range)
-          case _ => None
-        }).headOption.map(_.info)
-    }
-    else None
-
-  def completion_names(caret: Text.Offset): Option[Completion.Names] =
-    if (caret > 0 && !snapshot.is_outdated)
-    {
-      snapshot.select(Text.Range(caret - 1, caret + 1), Rendering.completion_names_elements, _ =>
+  def completion_names(range: Text.Range): Option[Completion.Names] =
+    if (snapshot.is_outdated) None
+    else {
+      snapshot.select(range, Rendering.completion_names_elements, _ =>
         {
           case Completion.Names.Info(names) => Some(names)
           case _ => None
         }).headOption.map(_.info)
     }
-    else None
 
-  def completion_context(caret: Text.Offset): Option[Completion.Context] =
-    if (caret > 0) {
-      snapshot.select(Text.Range(caret - 1, caret + 1), Rendering.completion_context_elements, _ =>
-        {
-          case Text.Info(_, elem)
-          if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
-            Some(Completion.Context.ML_inner)
-          case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
-            Some(Completion.Context(language, symbols, antiquotes))
-          case Text.Info(_, _) =>
-            Some(Completion.Context.inner)
-        }).headOption.map(_.info)
-    }
-    else None
+  def completion_context(range: Text.Range): Option[Completion.Context] =
+    snapshot.select(range, Rendering.completion_context_elements, _ =>
+      {
+        case Text.Info(_, elem)
+        if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
+          Some(Completion.Context.ML_inner)
+        case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
+          Some(Completion.Context(language, symbols, antiquotes))
+        case Text.Info(_, _) =>
+          Some(Completion.Context.inner)
+      }).headOption.map(_.info)
 
 
   /* command status overview */
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Feb 23 15:38:21 2014 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Feb 23 16:08:38 2014 +0100
@@ -224,9 +224,12 @@
 
   /* text background */
 
-  private def get_caret_range(): Text.Range =
-    if (caret_visible && text_area.isCaretVisible)
-      JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
+  private def get_caret_range(stretch: Boolean): Text.Range =
+    if (caret_visible && text_area.isCaretVisible) {
+      val caret = text_area.getCaretPosition
+      if (stretch) JEdit_Lib.stretch_point_range(buffer, caret)
+      else JEdit_Lib.point_range(buffer, caret)
+    }
     else Text.Range(-1)
 
   private val background_painter = new TextAreaExtension
@@ -306,7 +309,7 @@
     val clip_rect = gfx.getClipBounds
     val painter = text_area.getPainter
     val font_context = painter.getFontRenderContext
-    val caret_range = get_caret_range()
+    val caret_range = get_caret_range(false)
 
     var w = 0.0f
     var chunk = head
@@ -444,7 +447,7 @@
     {
       robust_rendering { rendering =>
         val painter = text_area.getPainter
-        val caret_range = get_caret_range()
+        val caret_range = get_caret_range(true)
 
         for (i <- 0 until physical_lines.length) {
           if (physical_lines(i) != -1) {
@@ -483,8 +486,8 @@
             for {
               caret <- caret_range.try_restrict(line_range)
               if !hyperlink_area.is_active
-              range <- rendering.completion_range(caret.start)
-              r <- JEdit_Lib.gfx_range(text_area, range)
+              names <- rendering.completion_names(caret)
+              r <- JEdit_Lib.gfx_range(text_area, names.range)
             } {
               gfx.setColor(painter.getCaretColor)
               gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)