# HG changeset patch # User wenzelm # Date 1393168118 -3600 # Node ID d73949233c2e05df9419ac8684fc109ba0cb7f8d # Parent 13b58baf994b64ea3d394b372b759395502d7e97 clarified stretch_point_range wrt. UTF-16 surrogates; tuned; diff -r 13b58baf994b -r d73949233c2e src/Tools/jEdit/src/completion_popup.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 { diff -r 13b58baf994b -r d73949233c2e src/Tools/jEdit/src/jedit_lib.scala --- 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 */ diff -r 13b58baf994b -r d73949233c2e src/Tools/jEdit/src/rendering.scala --- 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 */ diff -r 13b58baf994b -r d73949233c2e src/Tools/jEdit/src/rich_text_area.scala --- 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)