more robust caret painting wrt. surrogate characters;
authorwenzelm
Sat Jun 18 21:03:52 2011 +0200 (2011-06-18 ago)
changeset 4344890aec5043461
parent 43447 0ef3ec385b2b
child 43449 591598bc52bc
more robust caret painting wrt. surrogate characters;
discontinued glyphvector drawing -- less special cases;
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Jun 18 18:57:38 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Jun 18 21:03:52 2011 +0200
     1.3 @@ -302,6 +302,24 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* caret range */
     1.8 +
     1.9 +  def caret_range(): Text.Range =
    1.10 +    Isabelle.buffer_lock(model.buffer) {
    1.11 +      def text(i: Text.Offset): Char = model.buffer.getText(i, 1).charAt(0)
    1.12 +      val caret = text_area.getCaretPosition
    1.13 +      try {
    1.14 +        val c = text(caret)
    1.15 +        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(caret + 1)))
    1.16 +          Text.Range(caret, caret + 2)
    1.17 +        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(caret - 1)))
    1.18 +          Text.Range(caret - 1, caret + 1)
    1.19 +        else Text.Range(caret, caret + 1)
    1.20 +      }
    1.21 +      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(caret, caret + 1) }
    1.22 +    }
    1.23 +
    1.24 +
    1.25    /* caret handling */
    1.26  
    1.27    def selected_command(): Option[Command] =
     2.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 18:57:38 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 21:03:52 2011 +0200
     2.3 @@ -186,8 +186,8 @@
     2.4      result
     2.5    }
     2.6  
     2.7 -  private def paint_chunk_list(gfx: Graphics2D,
     2.8 -    offset: Text.Offset, caret_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
     2.9 +  private def paint_chunk_list(
    2.10 +    gfx: Graphics2D, offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
    2.11    {
    2.12      val clip_rect = gfx.getClipBounds
    2.13      val painter = text_area.getPainter
    2.14 @@ -207,6 +207,10 @@
    2.15          val chunk_font = chunk.style.getFont
    2.16          val chunk_color = chunk.style.getForegroundColor
    2.17  
    2.18 +        val caret_range =
    2.19 +          if (text_area.hasFocus) doc_view.caret_range()
    2.20 +          else Text.Range(-1)
    2.21 +
    2.22          val markup =
    2.23            for {
    2.24              x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color)
    2.25 @@ -214,13 +218,9 @@
    2.26            } yield y
    2.27  
    2.28          gfx.setFont(chunk_font)
    2.29 -        if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
    2.30 -            markup.forall(info => info.info.isEmpty) &&
    2.31 -            !chunk_range.contains(caret_offset)) {
    2.32 -          gfx.setColor(chunk_color)
    2.33 -          gfx.drawGlyphVector(chunk.gv, x + w, y)
    2.34 -        }
    2.35 -        else if (!markup.isEmpty) {
    2.36 +        if (markup.isEmpty)
    2.37 +          gfx.drawString(chunk.str, x.toInt, y.toInt)
    2.38 +        else {
    2.39            var x1 = x + w
    2.40            for {
    2.41              Text.Info(range, info) <-
    2.42 @@ -231,16 +231,18 @@
    2.43            } {
    2.44              val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
    2.45              gfx.setColor(info.getOrElse(chunk_color))
    2.46 -            if (range.contains(caret_offset)) {
    2.47 -              val astr = new AttributedString(str)
    2.48 -              val i = caret_offset - range.start
    2.49 -              astr.addAttribute(TextAttribute.FONT, chunk_font)
    2.50 -              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, i + 1)
    2.51 -              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, i + 1)
    2.52 -              gfx.drawString(astr.getIterator, x1.toInt, y.toInt)
    2.53 -            }
    2.54 -            else {
    2.55 -              gfx.drawString(str, x1.toInt, y.toInt)
    2.56 +
    2.57 +            range.try_restrict(caret_range) match {
    2.58 +              case Some(r) if !r.is_singularity =>
    2.59 +                val astr = new AttributedString(str)
    2.60 +                val i = r.start - range.start
    2.61 +                val j = r.stop - range.start
    2.62 +                astr.addAttribute(TextAttribute.FONT, chunk_font)
    2.63 +                astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
    2.64 +                astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
    2.65 +                gfx.drawString(astr.getIterator, x1.toInt, y.toInt)
    2.66 +              case _ =>
    2.67 +                gfx.drawString(str, x1.toInt, y.toInt)
    2.68              }
    2.69              x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
    2.70            }
    2.71 @@ -265,10 +267,6 @@
    2.72          val fm = text_area.getPainter.getFontMetrics
    2.73          var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
    2.74  
    2.75 -        val caret_offset =
    2.76 -          if (text_area.hasFocus) text_area.getCaretPosition
    2.77 -          else -1
    2.78 -
    2.79          val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
    2.80          for (i <- 0 until physical_lines.length) {
    2.81            if (physical_lines(i) != -1) {
    2.82 @@ -277,7 +275,7 @@
    2.83                  case None => x0
    2.84                  case Some(chunk) =>
    2.85                    gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
    2.86 -                  val w = paint_chunk_list(gfx, start(i), caret_offset, chunk, x0, y0).toInt
    2.87 +                  val w = paint_chunk_list(gfx, start(i), chunk, x0, y0).toInt
    2.88                    x0 + w.toInt
    2.89                }
    2.90              gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)