clarified stretch_point_range wrt. UTF-16 surrogates;
authorwenzelm
Sun Feb 23 16:08:38 2014 +0100 (2014-02-23 ago)
changeset 55690d73949233c2e
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
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sun Feb 23 15:38:21 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sun Feb 23 16:08:38 2014 +0100
     1.3 @@ -115,7 +115,9 @@
     1.4              val context =
     1.5                (PIDE.document_view(text_area) match {
     1.6                  case None => None
     1.7 -                case Some(doc_view) => doc_view.get_rendering().completion_context(caret)
     1.8 +                case Some(doc_view) =>
     1.9 +                  val rendering = doc_view.get_rendering()
    1.10 +                  rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret))
    1.11                }) getOrElse syntax.completion_context
    1.12  
    1.13              syntax.completion.complete(history, decode, explicit, text, context) match {
     2.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Feb 23 15:38:21 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Feb 23 16:08:38 2014 +0100
     2.3 @@ -177,6 +177,16 @@
     2.4        catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
     2.5      }
     2.6  
     2.7 +  def stretch_point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
     2.8 +  {
     2.9 +    val range = point_range(buffer, offset)
    2.10 +    val left = point_range(buffer, range.start - 1)
    2.11 +    val right = point_range(buffer, range.stop)
    2.12 +    val range1 = range.try_join(left) getOrElse range
    2.13 +    val range2 = range1.try_join(right) getOrElse range1
    2.14 +    range2
    2.15 +  }
    2.16 +
    2.17  
    2.18    /* visible text range */
    2.19  
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 15:38:21 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 16:08:38 2014 +0100
     3.3 @@ -273,41 +273,27 @@
     3.4  
     3.5    /* completion */
     3.6  
     3.7 -  def completion_range(caret: Text.Offset): Option[Text.Range] =
     3.8 -    if (!snapshot.is_outdated) {
     3.9 -      snapshot.select(Text.Range(caret - 1, caret + 1), Rendering.completion_names_elements, _ =>
    3.10 -        {
    3.11 -          case Completion.Names.Info(names) => Some(names.range)
    3.12 -          case _ => None
    3.13 -        }).headOption.map(_.info)
    3.14 -    }
    3.15 -    else None
    3.16 -
    3.17 -  def completion_names(caret: Text.Offset): Option[Completion.Names] =
    3.18 -    if (caret > 0 && !snapshot.is_outdated)
    3.19 -    {
    3.20 -      snapshot.select(Text.Range(caret - 1, caret + 1), Rendering.completion_names_elements, _ =>
    3.21 +  def completion_names(range: Text.Range): Option[Completion.Names] =
    3.22 +    if (snapshot.is_outdated) None
    3.23 +    else {
    3.24 +      snapshot.select(range, Rendering.completion_names_elements, _ =>
    3.25          {
    3.26            case Completion.Names.Info(names) => Some(names)
    3.27            case _ => None
    3.28          }).headOption.map(_.info)
    3.29      }
    3.30 -    else None
    3.31  
    3.32 -  def completion_context(caret: Text.Offset): Option[Completion.Context] =
    3.33 -    if (caret > 0) {
    3.34 -      snapshot.select(Text.Range(caret - 1, caret + 1), Rendering.completion_context_elements, _ =>
    3.35 -        {
    3.36 -          case Text.Info(_, elem)
    3.37 -          if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
    3.38 -            Some(Completion.Context.ML_inner)
    3.39 -          case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
    3.40 -            Some(Completion.Context(language, symbols, antiquotes))
    3.41 -          case Text.Info(_, _) =>
    3.42 -            Some(Completion.Context.inner)
    3.43 -        }).headOption.map(_.info)
    3.44 -    }
    3.45 -    else None
    3.46 +  def completion_context(range: Text.Range): Option[Completion.Context] =
    3.47 +    snapshot.select(range, Rendering.completion_context_elements, _ =>
    3.48 +      {
    3.49 +        case Text.Info(_, elem)
    3.50 +        if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
    3.51 +          Some(Completion.Context.ML_inner)
    3.52 +        case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
    3.53 +          Some(Completion.Context(language, symbols, antiquotes))
    3.54 +        case Text.Info(_, _) =>
    3.55 +          Some(Completion.Context.inner)
    3.56 +      }).headOption.map(_.info)
    3.57  
    3.58  
    3.59    /* command status overview */
     4.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Feb 23 15:38:21 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Feb 23 16:08:38 2014 +0100
     4.3 @@ -224,9 +224,12 @@
     4.4  
     4.5    /* text background */
     4.6  
     4.7 -  private def get_caret_range(): Text.Range =
     4.8 -    if (caret_visible && text_area.isCaretVisible)
     4.9 -      JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
    4.10 +  private def get_caret_range(stretch: Boolean): Text.Range =
    4.11 +    if (caret_visible && text_area.isCaretVisible) {
    4.12 +      val caret = text_area.getCaretPosition
    4.13 +      if (stretch) JEdit_Lib.stretch_point_range(buffer, caret)
    4.14 +      else JEdit_Lib.point_range(buffer, caret)
    4.15 +    }
    4.16      else Text.Range(-1)
    4.17  
    4.18    private val background_painter = new TextAreaExtension
    4.19 @@ -306,7 +309,7 @@
    4.20      val clip_rect = gfx.getClipBounds
    4.21      val painter = text_area.getPainter
    4.22      val font_context = painter.getFontRenderContext
    4.23 -    val caret_range = get_caret_range()
    4.24 +    val caret_range = get_caret_range(false)
    4.25  
    4.26      var w = 0.0f
    4.27      var chunk = head
    4.28 @@ -444,7 +447,7 @@
    4.29      {
    4.30        robust_rendering { rendering =>
    4.31          val painter = text_area.getPainter
    4.32 -        val caret_range = get_caret_range()
    4.33 +        val caret_range = get_caret_range(true)
    4.34  
    4.35          for (i <- 0 until physical_lines.length) {
    4.36            if (physical_lines(i) != -1) {
    4.37 @@ -483,8 +486,8 @@
    4.38              for {
    4.39                caret <- caret_range.try_restrict(line_range)
    4.40                if !hyperlink_area.is_active
    4.41 -              range <- rendering.completion_range(caret.start)
    4.42 -              r <- JEdit_Lib.gfx_range(text_area, range)
    4.43 +              names <- rendering.completion_names(caret)
    4.44 +              r <- JEdit_Lib.gfx_range(text_area, names.range)
    4.45              } {
    4.46                gfx.setColor(painter.getCaretColor)
    4.47                gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)