more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
authorwenzelm
Wed Jun 15 13:36:08 2011 +0200 (2011-06-15 ago)
changeset 43393f4141da52e92
parent 43392 fe4b8c52b1cc
child 43394 47e60a27a496
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
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	Wed Jun 15 11:41:49 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 13:36:08 2011 +0200
     1.3 @@ -396,7 +396,6 @@
     1.4      painter.addMouseMotionListener(mouse_motion_listener)
     1.5      text_area.addCaretListener(caret_listener)
     1.6      text_area.addLeftOfScrollBar(overview)
     1.7 -    if (text_area.isCaretBlinkEnabled) text_area.setCaretBlinkEnabled(false)
     1.8      session.commands_changed += main_actor
     1.9      session.global_settings += main_actor
    1.10    }
    1.11 @@ -406,7 +405,6 @@
    1.12      val painter = text_area.getPainter
    1.13      session.commands_changed -= main_actor
    1.14      session.global_settings -= main_actor
    1.15 -		text_area.setCaretBlinkEnabled(jEdit.getBooleanProperty("view.caretBlink"))
    1.16      text_area.removeFocusListener(focus_listener)
    1.17      text_area.getView.removeWindowListener(window_listener)
    1.18      painter.removeMouseMotionListener(mouse_motion_listener)
     2.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 11:41:49 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 13:36:08 2011 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  
     2.5  import isabelle._
     2.6  
     2.7 -import java.awt.Graphics2D
     2.8 +import java.awt.{Graphics2D, Shape}
     2.9  import java.awt.font.TextAttribute
    2.10  import java.text.AttributedString
    2.11  import java.util.ArrayList
    2.12 @@ -40,37 +40,31 @@
    2.13    private val orig_text_painter =
    2.14      pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
    2.15  
    2.16 -  private val orig_caret_painter =
    2.17 -    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintCaret")
    2.18  
    2.19 -
    2.20 -  /* painter snapshot */
    2.21 -
    2.22 -  @volatile private var _painter_snapshot: Option[Document.Snapshot] = None
    2.23 +  /* common painter state */
    2.24  
    2.25 -  private def painter_snapshot(): Document.Snapshot =
    2.26 -    _painter_snapshot match {
    2.27 -      case Some(snapshot) => snapshot
    2.28 -      case None => error("Missing document snapshot for text area painter")
    2.29 -    }
    2.30 +  @volatile private var painter_snapshot: Document.Snapshot = null
    2.31 +  @volatile private var painter_clip: Shape = null
    2.32  
    2.33 -  private val set_snapshot = new TextAreaExtension
    2.34 +  private val set_state = new TextAreaExtension
    2.35    {
    2.36      override def paintScreenLineRange(gfx: Graphics2D,
    2.37        first_line: Int, last_line: Int, physical_lines: Array[Int],
    2.38        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.39      {
    2.40 -      _painter_snapshot = Some(model.snapshot())
    2.41 +      painter_snapshot = model.snapshot()
    2.42 +      painter_clip = gfx.getClip
    2.43      }
    2.44    }
    2.45  
    2.46 -  private val reset_snapshot = new TextAreaExtension
    2.47 +  private val reset_state = new TextAreaExtension
    2.48    {
    2.49      override def paintScreenLineRange(gfx: Graphics2D,
    2.50        first_line: Int, last_line: Int, physical_lines: Array[Int],
    2.51        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.52      {
    2.53 -      _painter_snapshot = None
    2.54 +      painter_snapshot = null
    2.55 +      painter_clip = null
    2.56      }
    2.57    }
    2.58  
    2.59 @@ -84,7 +78,7 @@
    2.60        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.61      {
    2.62        Isabelle.swing_buffer_lock(buffer) {
    2.63 -        val snapshot = painter_snapshot()
    2.64 +        val snapshot = painter_snapshot
    2.65          val ascent = text_area.getPainter.getFontMetrics.getAscent
    2.66  
    2.67          for (i <- 0 until physical_lines.length) {
    2.68 @@ -158,6 +152,14 @@
    2.69  
    2.70    /* text */
    2.71  
    2.72 +  def char_width(): Int =
    2.73 +  {
    2.74 +    val painter = text_area.getPainter
    2.75 +    val font = painter.getFont
    2.76 +    val font_context = painter.getFontRenderContext
    2.77 +    font.getStringBounds(" ", font_context).getWidth.round.toInt
    2.78 +  }
    2.79 +
    2.80    private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
    2.81    {
    2.82      val painter = text_area.getPainter
    2.83 @@ -171,7 +173,7 @@
    2.84        else {
    2.85          val max = buffer.getIntegerProperty("maxLineLen", 0)
    2.86          if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
    2.87 -        else painter.getWidth - font.getStringBounds(" ", font_context).getWidth.round.toInt * 3
    2.88 +        else painter.getWidth - char_width() * 3
    2.89        }.toFloat
    2.90  
    2.91      val out = new ArrayList[Chunk]
    2.92 @@ -279,8 +281,6 @@
    2.93              gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
    2.94              orig_text_painter.paintValidLine(gfx,
    2.95                first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
    2.96 -            orig_caret_painter.paintValidLine(gfx,
    2.97 -              first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
    2.98              gfx.setClip(clip)
    2.99            }
   2.100            y0 += line_height
   2.101 @@ -290,31 +290,73 @@
   2.102    }
   2.103  
   2.104  
   2.105 +  /* caret -- outside of text range */
   2.106 +
   2.107 +  private class Caret_Painter(before: Boolean) extends TextAreaExtension
   2.108 +  {
   2.109 +    override def paintValidLine(gfx: Graphics2D,
   2.110 +      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   2.111 +    {
   2.112 +      if (before) gfx.clipRect(0, 0, 0, 0)
   2.113 +      else gfx.setClip(painter_clip)
   2.114 +    }
   2.115 +  }
   2.116 +
   2.117 +  private val before_caret_painter1 = new Caret_Painter(true)
   2.118 +  private val after_caret_painter1 = new Caret_Painter(false)
   2.119 +  private val before_caret_painter2 = new Caret_Painter(true)
   2.120 +  private val after_caret_painter2 = new Caret_Painter(false)
   2.121 +
   2.122 +  private val caret_painter = new TextAreaExtension
   2.123 +  {
   2.124 +    override def paintValidLine(gfx: Graphics2D,
   2.125 +      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   2.126 +    {
   2.127 +      if (text_area.hasFocus) {
   2.128 +        val caret = text_area.getCaretPosition
   2.129 +        if (start <= caret && caret == end - 1) {
   2.130 +          val painter = text_area.getPainter
   2.131 +          val fm = painter.getFontMetrics
   2.132 +
   2.133 +          val offset = caret - text_area.getLineStartOffset(physical_line)
   2.134 +          val x = text_area.offsetToXY(physical_line, offset).x
   2.135 +          gfx.setColor(painter.getCaretColor)
   2.136 +          gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1)
   2.137 +        }
   2.138 +      }
   2.139 +    }
   2.140 +  }
   2.141 +
   2.142 +
   2.143    /* activation */
   2.144  
   2.145    def activate()
   2.146    {
   2.147      val painter = text_area.getPainter
   2.148 -    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
   2.149 +    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
   2.150      painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   2.151      painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
   2.152 -    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
   2.153 +    painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
   2.154 +    painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
   2.155 +    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
   2.156 +    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
   2.157 +    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
   2.158 +    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
   2.159      painter.removeExtension(orig_text_painter)
   2.160 -    painter.removeExtension(orig_caret_painter)
   2.161    }
   2.162  
   2.163    def deactivate()
   2.164    {
   2.165      val painter = text_area.getPainter
   2.166 -    val caret_layer =
   2.167 -      if (painter.isBlockCaretEnabled) TextAreaPainter.BLOCK_CARET_LAYER
   2.168 -      else TextAreaPainter.CARET_LAYER
   2.169 -    painter.addExtension(caret_layer, orig_caret_painter)
   2.170 -    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   2.171 -    painter.removeExtension(reset_snapshot)
   2.172 +    painter.removeExtension(reset_state)
   2.173 +    painter.removeExtension(caret_painter)
   2.174 +    painter.removeExtension(after_caret_painter2)
   2.175 +    painter.removeExtension(before_caret_painter2)
   2.176 +    painter.removeExtension(after_caret_painter1)
   2.177 +    painter.removeExtension(before_caret_painter1)
   2.178      painter.removeExtension(text_painter)
   2.179      painter.removeExtension(background_painter)
   2.180 -    painter.removeExtension(set_snapshot)
   2.181 +    painter.removeExtension(set_state)
   2.182    }
   2.183  }
   2.184