src/Tools/jEdit/src/text_area_painter.scala
changeset 43393 f4141da52e92
parent 43392 fe4b8c52b1cc
child 43396 548a68eafaea
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 11:41:49 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 13:36:08 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import java.awt.Graphics2D
     1.8 +import java.awt.{Graphics2D, Shape}
     1.9  import java.awt.font.TextAttribute
    1.10  import java.text.AttributedString
    1.11  import java.util.ArrayList
    1.12 @@ -40,37 +40,31 @@
    1.13    private val orig_text_painter =
    1.14      pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
    1.15  
    1.16 -  private val orig_caret_painter =
    1.17 -    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintCaret")
    1.18  
    1.19 -
    1.20 -  /* painter snapshot */
    1.21 -
    1.22 -  @volatile private var _painter_snapshot: Option[Document.Snapshot] = None
    1.23 +  /* common painter state */
    1.24  
    1.25 -  private def painter_snapshot(): Document.Snapshot =
    1.26 -    _painter_snapshot match {
    1.27 -      case Some(snapshot) => snapshot
    1.28 -      case None => error("Missing document snapshot for text area painter")
    1.29 -    }
    1.30 +  @volatile private var painter_snapshot: Document.Snapshot = null
    1.31 +  @volatile private var painter_clip: Shape = null
    1.32  
    1.33 -  private val set_snapshot = new TextAreaExtension
    1.34 +  private val set_state = new TextAreaExtension
    1.35    {
    1.36      override def paintScreenLineRange(gfx: Graphics2D,
    1.37        first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.38        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.39      {
    1.40 -      _painter_snapshot = Some(model.snapshot())
    1.41 +      painter_snapshot = model.snapshot()
    1.42 +      painter_clip = gfx.getClip
    1.43      }
    1.44    }
    1.45  
    1.46 -  private val reset_snapshot = new TextAreaExtension
    1.47 +  private val reset_state = new TextAreaExtension
    1.48    {
    1.49      override def paintScreenLineRange(gfx: Graphics2D,
    1.50        first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.51        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.52      {
    1.53 -      _painter_snapshot = None
    1.54 +      painter_snapshot = null
    1.55 +      painter_clip = null
    1.56      }
    1.57    }
    1.58  
    1.59 @@ -84,7 +78,7 @@
    1.60        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.61      {
    1.62        Isabelle.swing_buffer_lock(buffer) {
    1.63 -        val snapshot = painter_snapshot()
    1.64 +        val snapshot = painter_snapshot
    1.65          val ascent = text_area.getPainter.getFontMetrics.getAscent
    1.66  
    1.67          for (i <- 0 until physical_lines.length) {
    1.68 @@ -158,6 +152,14 @@
    1.69  
    1.70    /* text */
    1.71  
    1.72 +  def char_width(): Int =
    1.73 +  {
    1.74 +    val painter = text_area.getPainter
    1.75 +    val font = painter.getFont
    1.76 +    val font_context = painter.getFontRenderContext
    1.77 +    font.getStringBounds(" ", font_context).getWidth.round.toInt
    1.78 +  }
    1.79 +
    1.80    private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
    1.81    {
    1.82      val painter = text_area.getPainter
    1.83 @@ -171,7 +173,7 @@
    1.84        else {
    1.85          val max = buffer.getIntegerProperty("maxLineLen", 0)
    1.86          if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
    1.87 -        else painter.getWidth - font.getStringBounds(" ", font_context).getWidth.round.toInt * 3
    1.88 +        else painter.getWidth - char_width() * 3
    1.89        }.toFloat
    1.90  
    1.91      val out = new ArrayList[Chunk]
    1.92 @@ -279,8 +281,6 @@
    1.93              gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
    1.94              orig_text_painter.paintValidLine(gfx,
    1.95                first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
    1.96 -            orig_caret_painter.paintValidLine(gfx,
    1.97 -              first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
    1.98              gfx.setClip(clip)
    1.99            }
   1.100            y0 += line_height
   1.101 @@ -290,31 +290,73 @@
   1.102    }
   1.103  
   1.104  
   1.105 +  /* caret -- outside of text range */
   1.106 +
   1.107 +  private class Caret_Painter(before: Boolean) extends TextAreaExtension
   1.108 +  {
   1.109 +    override def paintValidLine(gfx: Graphics2D,
   1.110 +      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   1.111 +    {
   1.112 +      if (before) gfx.clipRect(0, 0, 0, 0)
   1.113 +      else gfx.setClip(painter_clip)
   1.114 +    }
   1.115 +  }
   1.116 +
   1.117 +  private val before_caret_painter1 = new Caret_Painter(true)
   1.118 +  private val after_caret_painter1 = new Caret_Painter(false)
   1.119 +  private val before_caret_painter2 = new Caret_Painter(true)
   1.120 +  private val after_caret_painter2 = new Caret_Painter(false)
   1.121 +
   1.122 +  private val caret_painter = new TextAreaExtension
   1.123 +  {
   1.124 +    override def paintValidLine(gfx: Graphics2D,
   1.125 +      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   1.126 +    {
   1.127 +      if (text_area.hasFocus) {
   1.128 +        val caret = text_area.getCaretPosition
   1.129 +        if (start <= caret && caret == end - 1) {
   1.130 +          val painter = text_area.getPainter
   1.131 +          val fm = painter.getFontMetrics
   1.132 +
   1.133 +          val offset = caret - text_area.getLineStartOffset(physical_line)
   1.134 +          val x = text_area.offsetToXY(physical_line, offset).x
   1.135 +          gfx.setColor(painter.getCaretColor)
   1.136 +          gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1)
   1.137 +        }
   1.138 +      }
   1.139 +    }
   1.140 +  }
   1.141 +
   1.142 +
   1.143    /* activation */
   1.144  
   1.145    def activate()
   1.146    {
   1.147      val painter = text_area.getPainter
   1.148 -    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
   1.149 +    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
   1.150      painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   1.151      painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
   1.152 -    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
   1.153 +    painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
   1.154 +    painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
   1.155 +    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
   1.156 +    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
   1.157 +    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
   1.158 +    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
   1.159      painter.removeExtension(orig_text_painter)
   1.160 -    painter.removeExtension(orig_caret_painter)
   1.161    }
   1.162  
   1.163    def deactivate()
   1.164    {
   1.165      val painter = text_area.getPainter
   1.166 -    val caret_layer =
   1.167 -      if (painter.isBlockCaretEnabled) TextAreaPainter.BLOCK_CARET_LAYER
   1.168 -      else TextAreaPainter.CARET_LAYER
   1.169 -    painter.addExtension(caret_layer, orig_caret_painter)
   1.170 -    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   1.171 -    painter.removeExtension(reset_snapshot)
   1.172 +    painter.removeExtension(reset_state)
   1.173 +    painter.removeExtension(caret_painter)
   1.174 +    painter.removeExtension(after_caret_painter2)
   1.175 +    painter.removeExtension(before_caret_painter2)
   1.176 +    painter.removeExtension(after_caret_painter1)
   1.177 +    painter.removeExtension(before_caret_painter1)
   1.178      painter.removeExtension(text_painter)
   1.179      painter.removeExtension(background_painter)
   1.180 -    painter.removeExtension(set_snapshot)
   1.181 +    painter.removeExtension(set_state)
   1.182    }
   1.183  }
   1.184