# HG changeset patch # User wenzelm # Date 1305754762 -7200 # Node ID 19df8385f38d59e6d63eaddf9d5511bcade56169 # Parent 15727655bee270777e9fdd431993b24d3950a565 basic support for overpainting of text, imitating jEdit internals; diff -r 15727655bee2 -r 19df8385f38d src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Tue May 17 22:29:55 2011 +0200 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Wed May 18 23:39:22 2011 +0200 @@ -19,7 +19,7 @@ import javax.swing.event.{CaretListener, CaretEvent} import java.util.ArrayList -import org.gjt.sp.jedit.{jEdit, OperatingSystem} +import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug} import org.gjt.sp.jedit.gui.RolloverButton import org.gjt.sp.jedit.options.GutterOptionPane import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter} @@ -109,16 +109,28 @@ /* chunks */ - def line_chunks(physical: Int): java.util.List[Chunk] = + def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] = { + import scala.collection.JavaConversions._ + val buffer = text_area.getBuffer val painter = text_area.getPainter + val margin = wrap_margin().toFloat + val out = new ArrayList[Chunk] val handler = new DisplayTokenHandler - handler.init(painter.getStyles, painter.getFontRenderContext, painter, - new ArrayList[Chunk], wrap_margin().toFloat) - buffer.markTokens(physical, handler) - handler.getChunkList + + var result = Map[Text.Offset, Chunk]() + for (line <- physical_lines) { + out.clear + handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, margin) + buffer.markTokens(line, handler) + + val line_start = buffer.getLineStartOffset(line) + for (chunk <- handler.getChunkList.iterator) + result += (line_start + chunk.offset -> chunk) + } + result } @@ -345,6 +357,38 @@ } } + var use_text_painter = false + + private val text_painter = 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) + { + if (use_text_painter) { + Isabelle.swing_buffer_lock(model.buffer) { + val painter = text_area.getPainter + val fm = painter.getFontMetrics + + val all_chunks = line_chunks(Set[Int]() ++ physical_lines.iterator.filter(i => i != -1)) + + val x0 = text_area.getHorizontalOffset + var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent + for (i <- 0 until physical_lines.length) { + if (physical_lines(i) != -1) { + all_chunks.get(start(i)) match { + case Some(chunk) => + Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR) + case None => + } + } + y0 += line_height + } + } + } + } + } + private val gutter_painter = new TextAreaExtension { override def paintScreenLineRange(gfx: Graphics2D, @@ -514,6 +558,7 @@ { val painter = text_area.getPainter painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) + painter.addExtension(TextAreaPainter.TEXT_LAYER + 1, text_painter) text_area.getGutter.addExtension(gutter_painter) text_area.addFocusListener(focus_listener) text_area.getView.addWindowListener(window_listener) @@ -535,6 +580,7 @@ text_area.removeCaretListener(caret_listener) text_area.removeLeftOfScrollBar(overview) text_area.getGutter.removeExtension(gutter_painter) + painter.removeExtension(text_painter) painter.removeExtension(background_painter) exit_popup() }