clarified stretch_point_range wrt. UTF-16 surrogates;
tuned;
--- 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)