# HG changeset patch # User wenzelm # Date 1308044168 -7200 # Node ID 806878ae22193dd70fc413f021960c9e38bd9a06 # Parent 809de915155ff9d61c4eac2e57670ca965c20e5f separate module for text area painting; diff -r 809de915155f -r 806878ae2219 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Tue Jun 14 08:33:51 2011 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue Jun 14 11:36:08 2011 +0200 @@ -23,7 +23,7 @@ "src/raw_output_dockable.scala" "src/scala_console.scala" "src/session_dockable.scala" - "src/text_painter.scala" + "src/text_area_painter.scala" ) declare -a RESOURCES=( diff -r 809de915155f -r 806878ae2219 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Tue Jun 14 08:33:51 2011 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Tue Jun 14 11:36:08 2011 +0200 @@ -162,7 +162,8 @@ } } - private var highlight_range: Option[(Text.Range, Color)] = None + @volatile private var _highlight_range: Option[(Text.Range, Color)] = None + def highlight_range(): Option[(Text.Range, Color)] = _highlight_range /* CONTROL-mouse management */ @@ -172,12 +173,12 @@ private def exit_control() { exit_popup() - highlight_range = None + _highlight_range = None } private val focus_listener = new FocusAdapter { override def focusLost(e: FocusEvent) { - highlight_range = None // FIXME exit_control !? + _highlight_range = None // FIXME exit_control !? } } @@ -199,121 +200,20 @@ if (control) init_popup(snapshot, x, y) - highlight_range map { case (range, _) => invalidate_line_range(range) } - highlight_range = if (control) subexp_range(snapshot, x, y) else None - highlight_range map { case (range, _) => invalidate_line_range(range) } + _highlight_range map { case (range, _) => invalidate_line_range(range) } + _highlight_range = if (control) subexp_range(snapshot, x, y) else None + _highlight_range map { case (range, _) => invalidate_line_range(range) } } } } - /* TextArea painting */ - - @volatile private var _text_area_snapshot: Option[Document.Snapshot] = None - - def text_area_snapshot(): Document.Snapshot = - _text_area_snapshot match { - case Some(snapshot) => snapshot - case None => error("Missing text area snapshot") - } - - private val set_snapshot = 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) - { - _text_area_snapshot = Some(model.snapshot()) - } - } - - private val reset_snapshot = 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) - { - _text_area_snapshot = None - } - } - - private val background_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) - { - Isabelle.swing_buffer_lock(model.buffer) { - val snapshot = text_area_snapshot() - val ascent = text_area.getPainter.getFontMetrics.getAscent - - for (i <- 0 until physical_lines.length) { - if (physical_lines(i) != -1) { - val line_range = proper_line_range(start(i), end(i)) + /* text area painting */ - // background color: status - val cmds = snapshot.node.command_range(snapshot.revert(line_range)) - for { - (command, command_start) <- cmds if !command.is_ignored - val range = line_range.restrict(snapshot.convert(command.range + command_start)) - r <- Isabelle.gfx_range(text_area, range) - color <- Isabelle_Markup.status_color(snapshot, command) - } { - gfx.setColor(color) - gfx.fillRect(r.x, y + i * line_height, r.length, line_height) - } - - // background color (1): markup - for { - Text.Info(range, Some(color)) <- - snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator - r <- Isabelle.gfx_range(text_area, range) - } { - gfx.setColor(color) - gfx.fillRect(r.x, y + i * line_height, r.length, line_height) - } - - // background color (2): markup - for { - Text.Info(range, Some(color)) <- - snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator - r <- Isabelle.gfx_range(text_area, range) - } { - gfx.setColor(color) - gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4) - } + private val text_area_painter = new Text_Area_Painter(this) - // sub-expression highlighting -- potentially from other snapshot - highlight_range match { - case Some((range, color)) if line_range.overlaps(range) => - Isabelle.gfx_range(text_area, line_range.restrict(range)) match { - case None => - case Some(r) => - gfx.setColor(color) - gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) - } - case _ => - } - - // squiggly underline - for { - Text.Info(range, Some(color)) <- - snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator - r <- Isabelle.gfx_range(text_area, range) - } { - gfx.setColor(color) - val x0 = (r.x / 2) * 2 - val y0 = r.y + ascent + 1 - for (x1 <- Range(x0, x0 + r.length, 2)) { - val y1 = if (x1 % 4 < 2) y0 else y0 + 1 - gfx.drawLine(x1, y1, x1 + 1, y1) - } - } - } - } - } - } - + private val tooltip_painter = new TextAreaExtension + { override def getToolTipText(x: Int, y: Int): String = { Isabelle.swing_buffer_lock(model.buffer) { @@ -338,11 +238,6 @@ } } - val text_painter = new Text_Painter(this) - - - /* Gutter painting */ - private val gutter_painter = new TextAreaExtension { override def paintScreenLineRange(gfx: Graphics2D, @@ -511,12 +406,8 @@ private def activate() { val painter = text_area.getPainter - - painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot) - painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) - text_painter.activate() - painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot) - + painter.addExtension(TextAreaPainter.TEXT_LAYER, tooltip_painter) + text_area_painter.activate() text_area.getGutter.addExtension(gutter_painter) text_area.addFocusListener(focus_listener) text_area.getView.addWindowListener(window_listener) @@ -530,7 +421,6 @@ private def deactivate() { val painter = text_area.getPainter - session.commands_changed -= main_actor session.global_settings -= main_actor text_area.removeFocusListener(focus_listener) @@ -539,11 +429,8 @@ text_area.removeCaretListener(caret_listener) text_area.removeLeftOfScrollBar(overview) text_area.getGutter.removeExtension(gutter_painter) - - painter.removeExtension(reset_snapshot) - text_painter.deactivate() - painter.removeExtension(background_painter) - painter.removeExtension(set_snapshot) + text_area_painter.deactivate() + painter.removeExtension(tooltip_painter) exit_popup() } } diff -r 809de915155f -r 806878ae2219 src/Tools/jEdit/src/text_area_painter.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/text_area_painter.scala Tue Jun 14 11:36:08 2011 +0200 @@ -0,0 +1,286 @@ +/* Title: Tools/jEdit/src/text_area_painter.scala + Author: Makarius + +Painter setup for main 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_Area_Painter(doc_view: Document_View) +{ + private val model = doc_view.model + private val text_area = doc_view.text_area + + 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) + } + } + + + /* painter snapshot */ + + @volatile private var _painter_snapshot: Option[Document.Snapshot] = None + + private def painter_snapshot(): Document.Snapshot = + _painter_snapshot match { + case Some(snapshot) => snapshot + case None => error("Missing document snapshot for text area painter") + } + + private val set_snapshot = 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()) + } + } + + private val reset_snapshot = 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 + } + } + + + /* text background */ + + private val background_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) + { + Isabelle.swing_buffer_lock(model.buffer) { + val snapshot = painter_snapshot() + val ascent = text_area.getPainter.getFontMetrics.getAscent + + for (i <- 0 until physical_lines.length) { + if (physical_lines(i) != -1) { + val line_range = doc_view.proper_line_range(start(i), end(i)) + + // background color: status + val cmds = snapshot.node.command_range(snapshot.revert(line_range)) + for { + (command, command_start) <- cmds if !command.is_ignored + val range = line_range.restrict(snapshot.convert(command.range + command_start)) + r <- Isabelle.gfx_range(text_area, range) + color <- Isabelle_Markup.status_color(snapshot, command) + } { + gfx.setColor(color) + gfx.fillRect(r.x, y + i * line_height, r.length, line_height) + } + + // background color (1): markup + for { + Text.Info(range, Some(color)) <- + snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator + r <- Isabelle.gfx_range(text_area, range) + } { + gfx.setColor(color) + gfx.fillRect(r.x, y + i * line_height, r.length, line_height) + } + + // background color (2): markup + for { + Text.Info(range, Some(color)) <- + snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator + r <- Isabelle.gfx_range(text_area, range) + } { + gfx.setColor(color) + gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4) + } + + // sub-expression highlighting -- potentially from other snapshot + doc_view.highlight_range match { + case Some((range, color)) if line_range.overlaps(range) => + Isabelle.gfx_range(text_area, line_range.restrict(range)) match { + case None => + case Some(r) => + gfx.setColor(color) + gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) + } + case _ => + } + + // squiggly underline + for { + Text.Info(range, Some(color)) <- + snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator + r <- Isabelle.gfx_range(text_area, range) + } { + gfx.setColor(color) + val x0 = (r.x / 2) * 2 + val y0 = r.y + ascent + 1 + for (x1 <- Range(x0, x0 + r.length, 2)) { + val y1 = if (x1 % 4 < 2) y0 else y0 + 1 + gfx.drawLine(x1, y1, x1 + 1, y1) + } + } + } + } + } + } + } + + + /* text */ + + 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_start: Int, line_height: Int) + { + val buffer = text_area.getBuffer + Isabelle.swing_buffer_lock(buffer) { + val painter = text_area.getPainter + val font = painter.getFont + val font_context = painter.getFontRenderContext + val font_metrics = painter.getFontMetrics + + def paint_chunk_list(head_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float = + { + val clip_rect = gfx.getClipBounds + + var w = 0.0f + var offset = head_offset + var chunk = head + while (chunk != null) { + val chunk_length = if (chunk.str == null) 0 else chunk.str.length + + if (x + w + chunk.width > clip_rect.x && + x + w < clip_rect.x + clip_rect.width && + chunk.accessable && chunk.visible) + { + val chunk_range = Text.Range(offset, offset + chunk_length) + val chunk_font = chunk.style.getFont + val chunk_color = chunk.style.getForegroundColor + + val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground) + + gfx.setFont(chunk_font) + if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null && + markup.forall(info => info.info.isEmpty)) { + gfx.setColor(chunk_color) + gfx.drawGlyphVector(chunk.gv, x + w, y) + } + else { + var xpos = x + w + for (Text.Info(range, info) <- markup) { + val str = chunk.str.substring(range.start - offset, range.stop - offset) + gfx.setColor(info.getOrElse(chunk_color)) + gfx.drawString(str, xpos.toInt, y.toInt) + xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat + } + } + } + w += chunk.width + offset += chunk_length + chunk = chunk.next.asInstanceOf[Chunk] + } + w + } + + // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged + // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength + val char_width = font.getStringBounds(" ", font_context).getWidth.round.toInt + val soft_wrap = buffer.getStringProperty("wrap") == "soft" + val wrap_margin = + { + val max = buffer.getIntegerProperty("maxLineLen", 0) + if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt + else if (soft_wrap) painter.getWidth - char_width * 3 + else 0 + }.toFloat + + val line_infos: Map[Text.Offset, Chunk] = + { + val out = new ArrayList[Chunk] + val handler = new DisplayTokenHandler + val margin = if (soft_wrap) wrap_margin else 0.0f + + var result = Map[Text.Offset, Chunk]() + for (line <- physical_lines.iterator.filter(i => i != -1)) { + out.clear + handler.init(painter.getStyles, font_context, painter, out, margin) + buffer.markTokens(line, handler) + + val line_start = buffer.getLineStartOffset(line) + for (i <- 0 until out.size) { + val chunk = out.get(i) + result += (line_start + chunk.offset -> chunk) + } + } + result + } + + val clip = gfx.getClip + val x0 = text_area.getHorizontalOffset + var y0 = + y_start + font_metrics.getHeight - (font_metrics.getLeading + 1) - font_metrics.getDescent + + for (i <- 0 until physical_lines.length) { + if (physical_lines(i) != -1) { + line_infos.get(start(i)) match { + case Some(chunk) => + val w = paint_chunk_list(start(i), chunk, x0, y0).toInt + gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE) + orig_text_painter.paintValidLine(gfx, + first_line + i, physical_lines(i), start(i), end(i), y_start + line_height * i) + gfx.setClip(clip) + + case None => + } + } + y0 += line_height + } + } + } + } + + + /* activation */ + + def activate() + { + val painter = text_area.getPainter + painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot) + painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) + painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter) + painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot) + painter.removeExtension(orig_text_painter) + } + + def deactivate() + { + val painter = text_area.getPainter + painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) + painter.removeExtension(reset_snapshot) + painter.removeExtension(text_painter) + painter.removeExtension(background_painter) + painter.removeExtension(set_snapshot) + } +} + diff -r 809de915155f -r 806878ae2219 src/Tools/jEdit/src/text_painter.scala --- a/src/Tools/jEdit/src/text_painter.scala Tue Jun 14 08:33:51 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,162 +0,0 @@ -/* 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(doc_view: Document_View) extends TextAreaExtension -{ - private val text_area = doc_view.text_area - - 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) - } - } - - override def paintScreenLineRange(gfx: Graphics2D, - first_line: Int, last_line: Int, physical_lines: Array[Int], - start: Array[Int], end: Array[Int], y_start: Int, line_height: Int) - { - val buffer = text_area.getBuffer - Isabelle.swing_buffer_lock(buffer) { - val painter = text_area.getPainter - val font = painter.getFont - val font_context = painter.getFontRenderContext - val font_metrics = painter.getFontMetrics - - def paint_chunk_list(head_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float = - { - val clip_rect = gfx.getClipBounds - - var w = 0.0f - var offset = head_offset - var chunk = head - while (chunk != null) { - val chunk_length = if (chunk.str == null) 0 else chunk.str.length - - if (x + w + chunk.width > clip_rect.x && - x + w < clip_rect.x + clip_rect.width && - chunk.accessable && chunk.visible) - { - val chunk_range = Text.Range(offset, offset + chunk_length) - val chunk_font = chunk.style.getFont - val chunk_color = chunk.style.getForegroundColor - - val markup = - doc_view.text_area_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground) - - gfx.setFont(chunk_font) - if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null && - markup.forall(info => info.info.isEmpty)) { - gfx.setColor(chunk_color) - gfx.drawGlyphVector(chunk.gv, x + w, y) - } - else { - var xpos = x + w - for (Text.Info(range, info) <- markup) { - val str = chunk.str.substring(range.start - offset, range.stop - offset) - gfx.setColor(info.getOrElse(chunk_color)) - gfx.drawString(str, xpos.toInt, y.toInt) - xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat - } - } - } - w += chunk.width - offset += chunk_length - chunk = chunk.next.asInstanceOf[Chunk] - } - w - } - - // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged - // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength - val char_width = font.getStringBounds(" ", font_context).getWidth.round.toInt - val soft_wrap = buffer.getStringProperty("wrap") == "soft" - val wrap_margin = - { - val max = buffer.getIntegerProperty("maxLineLen", 0) - if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt - else if (soft_wrap) painter.getWidth - char_width * 3 - else 0 - }.toFloat - - val line_infos: Map[Text.Offset, Chunk] = - { - val out = new ArrayList[Chunk] - val handler = new DisplayTokenHandler - val margin = if (soft_wrap) wrap_margin else 0.0f - - var result = Map[Text.Offset, Chunk]() - for (line <- physical_lines.iterator.filter(i => i != -1)) { - out.clear - handler.init(painter.getStyles, font_context, painter, out, margin) - buffer.markTokens(line, handler) - - val line_start = buffer.getLineStartOffset(line) - for (i <- 0 until out.size) { - val chunk = out.get(i) - result += (line_start + chunk.offset -> chunk) - } - } - result - } - - val clip = gfx.getClip - val x0 = text_area.getHorizontalOffset - var y0 = - y_start + font_metrics.getHeight - (font_metrics.getLeading + 1) - font_metrics.getDescent - - for (i <- 0 until physical_lines.length) { - if (physical_lines(i) != -1) { - line_infos.get(start(i)) match { - case Some(chunk) => - val w = paint_chunk_list(start(i), chunk, x0, y0).toInt - gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE) - orig_text_painter.paintValidLine(gfx, - first_line + i, physical_lines(i), start(i), end(i), y_start + line_height * i) - gfx.setClip(clip) - - case None => - } - } - y0 += 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) - } -} -