# HG changeset patch # User wenzelm # Date 1308137768 -7200 # Node ID f4141da52e920e943281b38d7cc971eee3353ad7 # Parent fe4b8c52b1cc84fd5ef29924163521b2f295783e more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally); diff -r fe4b8c52b1cc -r f4141da52e92 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Wed Jun 15 11:41:49 2011 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Wed Jun 15 13:36:08 2011 +0200 @@ -396,7 +396,6 @@ painter.addMouseMotionListener(mouse_motion_listener) text_area.addCaretListener(caret_listener) text_area.addLeftOfScrollBar(overview) - if (text_area.isCaretBlinkEnabled) text_area.setCaretBlinkEnabled(false) session.commands_changed += main_actor session.global_settings += main_actor } @@ -406,7 +405,6 @@ val painter = text_area.getPainter session.commands_changed -= main_actor session.global_settings -= main_actor - text_area.setCaretBlinkEnabled(jEdit.getBooleanProperty("view.caretBlink")) text_area.removeFocusListener(focus_listener) text_area.getView.removeWindowListener(window_listener) painter.removeMouseMotionListener(mouse_motion_listener) diff -r fe4b8c52b1cc -r f4141da52e92 src/Tools/jEdit/src/text_area_painter.scala --- a/src/Tools/jEdit/src/text_area_painter.scala Wed Jun 15 11:41:49 2011 +0200 +++ b/src/Tools/jEdit/src/text_area_painter.scala Wed Jun 15 13:36:08 2011 +0200 @@ -9,7 +9,7 @@ import isabelle._ -import java.awt.Graphics2D +import java.awt.{Graphics2D, Shape} import java.awt.font.TextAttribute import java.text.AttributedString import java.util.ArrayList @@ -40,37 +40,31 @@ private val orig_text_painter = pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText") - private val orig_caret_painter = - pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintCaret") - - /* painter snapshot */ - - @volatile private var _painter_snapshot: Option[Document.Snapshot] = None + /* common painter state */ - private def painter_snapshot(): Document.Snapshot = - _painter_snapshot match { - case Some(snapshot) => snapshot - case None => error("Missing document snapshot for text area painter") - } + @volatile private var painter_snapshot: Document.Snapshot = null + @volatile private var painter_clip: Shape = null - private val set_snapshot = new TextAreaExtension + private val set_state = new TextAreaExtension { override def paintScreenLineRange(gfx: Graphics2D, first_line: Int, last_line: Int, physical_lines: Array[Int], start: Array[Int], end: Array[Int], y: Int, line_height: Int) { - _painter_snapshot = Some(model.snapshot()) + painter_snapshot = model.snapshot() + painter_clip = gfx.getClip } } - private val reset_snapshot = new TextAreaExtension + private val reset_state = new TextAreaExtension { override def paintScreenLineRange(gfx: Graphics2D, first_line: Int, last_line: Int, physical_lines: Array[Int], start: Array[Int], end: Array[Int], y: Int, line_height: Int) { - _painter_snapshot = None + painter_snapshot = null + painter_clip = null } } @@ -84,7 +78,7 @@ start: Array[Int], end: Array[Int], y: Int, line_height: Int) { Isabelle.swing_buffer_lock(buffer) { - val snapshot = painter_snapshot() + val snapshot = painter_snapshot val ascent = text_area.getPainter.getFontMetrics.getAscent for (i <- 0 until physical_lines.length) { @@ -158,6 +152,14 @@ /* text */ + def char_width(): Int = + { + val painter = text_area.getPainter + val font = painter.getFont + val font_context = painter.getFontRenderContext + font.getStringBounds(" ", font_context).getWidth.round.toInt + } + private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] = { val painter = text_area.getPainter @@ -171,7 +173,7 @@ else { val max = buffer.getIntegerProperty("maxLineLen", 0) if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt - else painter.getWidth - font.getStringBounds(" ", font_context).getWidth.round.toInt * 3 + else painter.getWidth - char_width() * 3 }.toFloat val out = new ArrayList[Chunk] @@ -279,8 +281,6 @@ gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE) orig_text_painter.paintValidLine(gfx, first_line + i, physical_lines(i), start(i), end(i), y + line_height * i) - orig_caret_painter.paintValidLine(gfx, - first_line + i, physical_lines(i), start(i), end(i), y + line_height * i) gfx.setClip(clip) } y0 += line_height @@ -290,31 +290,73 @@ } + /* caret -- outside of text range */ + + private class Caret_Painter(before: Boolean) extends TextAreaExtension + { + override def paintValidLine(gfx: Graphics2D, + screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) + { + if (before) gfx.clipRect(0, 0, 0, 0) + else gfx.setClip(painter_clip) + } + } + + private val before_caret_painter1 = new Caret_Painter(true) + private val after_caret_painter1 = new Caret_Painter(false) + private val before_caret_painter2 = new Caret_Painter(true) + private val after_caret_painter2 = new Caret_Painter(false) + + private val caret_painter = new TextAreaExtension + { + override def paintValidLine(gfx: Graphics2D, + screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) + { + if (text_area.hasFocus) { + val caret = text_area.getCaretPosition + if (start <= caret && caret == end - 1) { + val painter = text_area.getPainter + val fm = painter.getFontMetrics + + val offset = caret - text_area.getLineStartOffset(physical_line) + val x = text_area.offsetToXY(physical_line, offset).x + gfx.setColor(painter.getCaretColor) + gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1) + } + } + } + } + + /* activation */ def activate() { val painter = text_area.getPainter - painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot) + painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state) painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter) - painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot) + painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1) + painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1) + painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2) + painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2) + painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter) + painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state) painter.removeExtension(orig_text_painter) - painter.removeExtension(orig_caret_painter) } def deactivate() { val painter = text_area.getPainter - val caret_layer = - if (painter.isBlockCaretEnabled) TextAreaPainter.BLOCK_CARET_LAYER - else TextAreaPainter.CARET_LAYER - painter.addExtension(caret_layer, orig_caret_painter) - painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) - painter.removeExtension(reset_snapshot) + painter.removeExtension(reset_state) + painter.removeExtension(caret_painter) + painter.removeExtension(after_caret_painter2) + painter.removeExtension(before_caret_painter2) + painter.removeExtension(after_caret_painter1) + painter.removeExtension(before_caret_painter1) painter.removeExtension(text_painter) painter.removeExtension(background_painter) - painter.removeExtension(set_snapshot) + painter.removeExtension(set_state) } }