src/Tools/jEdit/src/text_area_painter.scala
changeset 43392 fe4b8c52b1cc
parent 43383 63fc6b5ef8ac
child 43393 f4141da52e92
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Tue Jun 14 21:41:00 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 11:41:49 2011 +0200
     1.3 @@ -10,11 +10,13 @@
     1.4  import isabelle._
     1.5  
     1.6  import java.awt.Graphics2D
     1.7 +import java.awt.font.TextAttribute
     1.8 +import java.text.AttributedString
     1.9  import java.util.ArrayList
    1.10  
    1.11  import org.gjt.sp.jedit.Debug
    1.12  import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
    1.13 -import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
    1.14 +import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, JEditTextArea}
    1.15  
    1.16  
    1.17  class Text_Area_Painter(doc_view: Document_View)
    1.18 @@ -23,9 +25,11 @@
    1.19    private val buffer = model.buffer
    1.20    private val text_area = doc_view.text_area
    1.21  
    1.22 -  private val orig_text_painter: TextAreaExtension =
    1.23 +
    1.24 +  /* original painters */
    1.25 +
    1.26 +  private def pick_extension(name: String): TextAreaExtension =
    1.27    {
    1.28 -    val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText"
    1.29      text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
    1.30      match {
    1.31        case List(x) => x
    1.32 @@ -33,6 +37,12 @@
    1.33      }
    1.34    }
    1.35  
    1.36 +  private val orig_text_painter =
    1.37 +    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
    1.38 +
    1.39 +  private val orig_caret_painter =
    1.40 +    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintCaret")
    1.41 +
    1.42  
    1.43    /* painter snapshot */
    1.44  
    1.45 @@ -183,10 +193,11 @@
    1.46    }
    1.47  
    1.48    private def paint_chunk_list(gfx: Graphics2D,
    1.49 -    offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
    1.50 +    offset: Text.Offset, caret_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
    1.51    {
    1.52      val clip_rect = gfx.getClipBounds
    1.53 -    val font_context = text_area.getPainter.getFontRenderContext
    1.54 +    val painter = text_area.getPainter
    1.55 +    val font_context = painter.getFontRenderContext
    1.56  
    1.57      var w = 0.0f
    1.58      var chunk_offset = offset
    1.59 @@ -206,7 +217,8 @@
    1.60  
    1.61          gfx.setFont(chunk_font)
    1.62          if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
    1.63 -            markup.forall(info => info.info.isEmpty)) {
    1.64 +            markup.forall(info => info.info.isEmpty) &&
    1.65 +            !chunk_range.contains(caret_offset)) {
    1.66            gfx.setColor(chunk_color)
    1.67            gfx.drawGlyphVector(chunk.gv, x + w, y)
    1.68          }
    1.69 @@ -215,7 +227,17 @@
    1.70            for (Text.Info(range, info) <- markup) {
    1.71              val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
    1.72              gfx.setColor(info.getOrElse(chunk_color))
    1.73 -            gfx.drawString(str, x1.toInt, y.toInt)
    1.74 +            if (range.contains(caret_offset)) {
    1.75 +              val astr = new AttributedString(str)
    1.76 +              val i = caret_offset - range.start
    1.77 +              astr.addAttribute(TextAttribute.FONT, chunk_font)
    1.78 +              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, i + 1)
    1.79 +              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, i + 1)
    1.80 +              gfx.drawString(astr.getIterator, x1.toInt, y.toInt)
    1.81 +            }
    1.82 +            else {
    1.83 +              gfx.drawString(str, x1.toInt, y.toInt)
    1.84 +            }
    1.85              x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
    1.86            }
    1.87          }
    1.88 @@ -239,18 +261,27 @@
    1.89          val fm = text_area.getPainter.getFontMetrics
    1.90          var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
    1.91  
    1.92 +        val caret_offset =
    1.93 +          if (text_area.hasFocus) text_area.getCaretPosition
    1.94 +          else -1
    1.95 +
    1.96          val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
    1.97          for (i <- 0 until physical_lines.length) {
    1.98            if (physical_lines(i) != -1) {
    1.99 -            infos.get(start(i)) match {
   1.100 -              case Some(chunk) =>
   1.101 -                val w = paint_chunk_list(gfx, start(i), chunk, x0, y0).toInt
   1.102 -                gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   1.103 -                orig_text_painter.paintValidLine(gfx,
   1.104 -                  first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
   1.105 -                gfx.setClip(clip)
   1.106 -              case None =>
   1.107 -            }
   1.108 +            val x1 =
   1.109 +              infos.get(start(i)) match {
   1.110 +                case None => x0
   1.111 +                case Some(chunk) =>
   1.112 +                  gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
   1.113 +                  val w = paint_chunk_list(gfx, start(i), caret_offset, chunk, x0, y0).toInt
   1.114 +                  x0 + w.toInt
   1.115 +              }
   1.116 +            gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   1.117 +            orig_text_painter.paintValidLine(gfx,
   1.118 +              first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
   1.119 +            orig_caret_painter.paintValidLine(gfx,
   1.120 +              first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
   1.121 +            gfx.setClip(clip)
   1.122            }
   1.123            y0 += line_height
   1.124          }
   1.125 @@ -269,11 +300,16 @@
   1.126      painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
   1.127      painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
   1.128      painter.removeExtension(orig_text_painter)
   1.129 +    painter.removeExtension(orig_caret_painter)
   1.130    }
   1.131  
   1.132    def deactivate()
   1.133    {
   1.134      val painter = text_area.getPainter
   1.135 +    val caret_layer =
   1.136 +      if (painter.isBlockCaretEnabled) TextAreaPainter.BLOCK_CARET_LAYER
   1.137 +      else TextAreaPainter.CARET_LAYER
   1.138 +    painter.addExtension(caret_layer, orig_caret_painter)
   1.139      painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   1.140      painter.removeExtension(reset_snapshot)
   1.141      painter.removeExtension(text_painter)