# HG changeset patch # User wenzelm # Date 1307902129 -7200 # Node ID 4c86b3405010abcda1bed3d814dab4d0265f1e53 # Parent 0dc67b3cf8a5ad44261c70ffee1efbdcdb07520d separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance; diff -r 0dc67b3cf8a5 -r 4c86b3405010 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Sun Jun 12 16:19:29 2011 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Sun Jun 12 20:08:49 2011 +0200 @@ -23,6 +23,7 @@ "src/raw_output_dockable.scala" "src/scala_console.scala" "src/session_dockable.scala" + "src/text_painter.scala" ) declare -a RESOURCES=( diff -r 0dc67b3cf8a5 -r 4c86b3405010 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Sun Jun 12 16:19:29 2011 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Sun Jun 12 20:08:49 2011 +0200 @@ -17,13 +17,12 @@ FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory} import javax.swing.event.{CaretListener, CaretEvent} -import java.util.ArrayList 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} -import org.gjt.sp.jedit.syntax.{SyntaxStyle, DisplayTokenHandler, Chunk, Token} +import org.gjt.sp.jedit.syntax.{SyntaxStyle} object Document_View @@ -88,52 +87,6 @@ } - /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */ - - def wrap_margin(): Int = - { - val buffer = text_area.getBuffer - val painter = text_area.getPainter - val font = painter.getFont - val font_context = painter.getFontRenderContext - - val soft_wrap = buffer.getStringProperty("wrap") == "soft" - val max = buffer.getIntegerProperty("maxLineLen", 0) - - if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt - else if (soft_wrap) - painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3 - else 0 - } - - - /* chunks */ - - 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 - - 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 - } - - /* visible line ranges */ // simplify slightly odd result of TextArea.getScreenLineEndOffset etc. @@ -357,37 +310,7 @@ } } - 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 - } - } - } - } - } + val text_painter = new Text_Painter(model, text_area) private val gutter_painter = new TextAreaExtension { @@ -558,7 +481,7 @@ { val painter = text_area.getPainter painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) - painter.addExtension(TextAreaPainter.TEXT_LAYER + 1, text_painter) + text_painter.activate() text_area.getGutter.addExtension(gutter_painter) text_area.addFocusListener(focus_listener) text_area.getView.addWindowListener(window_listener) @@ -580,7 +503,7 @@ text_area.removeCaretListener(caret_listener) text_area.removeLeftOfScrollBar(overview) text_area.getGutter.removeExtension(gutter_painter) - painter.removeExtension(text_painter) + text_painter.deactivate() painter.removeExtension(background_painter) exit_popup() } diff -r 0dc67b3cf8a5 -r 4c86b3405010 src/Tools/jEdit/src/text_painter.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/text_painter.scala Sun Jun 12 20:08:49 2011 +0200 @@ -0,0 +1,128 @@ +/* Title: Tools/jEdit/src/text_painter.scala + Author: Makarius + +Replacement painter for jEdit text area. +*/ + +package isabelle.jedit + + +import isabelle._ + +import java.awt.{Graphics, Graphics2D} +import java.util.ArrayList + +import org.gjt.sp.jedit.Debug +import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk} +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter} + + +class Text_Painter(model: Document_Model, text_area: JEditTextArea) extends TextAreaExtension +{ + private val orig_text_painter: TextAreaExtension = + { + val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText" + text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList + match { + case List(x) => x + case _ => error("Expected exactly one " + name) + } + } + + + /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */ + + private def wrap_margin(): Int = + { + val buffer = text_area.getBuffer + val painter = text_area.getPainter + val font = painter.getFont + val font_context = painter.getFontRenderContext + + val soft_wrap = buffer.getStringProperty("wrap") == "soft" + val max = buffer.getIntegerProperty("maxLineLen", 0) + + if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt + else if (soft_wrap) + painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3 + else 0 + } + + + /* chunks */ + + private 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 + + 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 + } + + + var use = false + + 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) { + 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 + } + } + } + else + orig_text_painter.paintScreenLineRange( + gfx, first_line, last_line, physical_lines, start, end, y, line_height) + } + + + /* activation */ + + def activate() + { + val painter = text_area.getPainter + painter.removeExtension(orig_text_painter) + painter.addExtension(TextAreaPainter.TEXT_LAYER, this) + } + + def deactivate() + { + val painter = text_area.getPainter + painter.removeExtension(this) + painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) + } +} +