# HG changeset patch # User wenzelm # Date 1308059881 -7200 # Node ID 328dcc5cc43f57e2ab5cd2594a1b3473f03757a6 # Parent 9cd4b4ecb4dd2d72ffc4cfa991a5101ce6b9fb9f# Parent 34492601c0e003f006eb8adce8cf993be2718693 merged diff -r 9cd4b4ecb4dd -r 328dcc5cc43f src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Tue Jun 14 13:50:54 2011 +0200 +++ b/src/Pure/General/markup.scala Tue Jun 14 15:58:01 2011 +0200 @@ -167,6 +167,7 @@ val XNUM = "xnum" val XSTR = "xstr" val LITERAL = "literal" + val INNER_STRING = "inner_string" val INNER_COMMENT = "inner_comment" val TOKEN_RANGE = "token_range" diff -r 9cd4b4ecb4dd -r 328dcc5cc43f src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Tue Jun 14 13:50:54 2011 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue Jun 14 15:58:01 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=( @@ -166,17 +166,27 @@ TARGET="dist/jars/Isabelle-jEdit.jar" +declare -a UPDATED=() + if [ "$BUILD_JARS" = jars_fresh ]; then OUTDATED=true else OUTDATED=false if [ ! -e "$TARGET" ]; then OUTDATED=true - elif [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then - for SOURCE in "${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}" + else + if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then + declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}") + else + declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}") + fi + for DEP in "${DEPS[@]}" do - [ ! -e "$SOURCE" ] && fail "Missing file: $SOURCE" - [ "$SOURCE" -nt "$TARGET" ] && OUTDATED=true + [ ! -e "$DEP" ] && fail "Missing file: $DEP" + [ "$DEP" -nt "$TARGET" ] && { + OUTDATED=true + UPDATED["${#UPDATED[@]}"]="$DEP" + } done fi fi @@ -186,6 +196,14 @@ if [ "$OUTDATED" = true ] then + [ "${#UPDATED[@]}" -gt 0 ] && { + echo "Rebuild due to updated file dependencies:" + for FILE in "${UPDATED[@]}" + do + echo " $FILE" + done + } + [ -z "$SCALA_HOME" ] && fail "Unknown SCALA_HOME -- Scala unavailable" [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \ diff -r 9cd4b4ecb4dd -r 328dcc5cc43f src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Tue Jun 14 13:50:54 2011 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Tue Jun 14 15:58:01 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.LINE_BACKGROUND_LAYER + 1, 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 9cd4b4ecb4dd -r 328dcc5cc43f src/Tools/jEdit/src/isabelle_markup.scala --- a/src/Tools/jEdit/src/isabelle_markup.scala Tue Jun 14 13:50:54 2011 +0200 +++ b/src/Tools/jEdit/src/isabelle_markup.scala Tue Jun 14 15:58:01 2011 +0200 @@ -11,6 +11,7 @@ import java.awt.Color +import org.lobobrowser.util.gui.ColorFactory import org.gjt.sp.jedit.syntax.Token @@ -20,6 +21,8 @@ // see http://www.w3schools.com/css/css_colornames.asp + def get_color(s: String): Color = ColorFactory.getInstance.getColor(s) + val outdated_color = new Color(240, 240, 240) val unfinished_color = new Color(255, 228, 225) @@ -30,9 +33,8 @@ val bad_color = new Color(255, 106, 106, 100) val hilite_color = new Color(255, 204, 102, 100) - val free_color = new Color(0, 0, 0xFF) - val skolem_color = new Color(0xD2, 0x69, 0x1E) - val bound_color = new Color(0, 0x80, 0) + val keyword1_color = get_color("#006699") + val keyword2_color = get_color("#009966") class Icon(val priority: Int, val icon: javax.swing.Icon) { @@ -106,11 +108,33 @@ case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color } + private val foreground_colors: Map[String, Color] = + Map( + Markup.TCLASS -> get_color("red"), + Markup.TFREE -> get_color("#A020F0"), + Markup.TVAR -> get_color("#A020F0"), + Markup.CONST -> get_color("dimgrey"), + Markup.FREE -> get_color("blue"), + Markup.SKOLEM -> get_color("#D2691E"), + Markup.BOUND -> get_color("green"), + Markup.VAR -> get_color("#00009B"), + Markup.INNER_STRING -> get_color("#D2691E"), + Markup.INNER_COMMENT -> get_color("#8B0000"), + Markup.DYNAMIC_FACT -> get_color("yellowgreen"), + Markup.LITERAL -> keyword1_color, + Markup.ML_KEYWORD -> keyword1_color, + Markup.ML_DELIMITER -> get_color("black"), + Markup.ML_NUMERAL -> get_color("red"), + Markup.ML_CHAR -> get_color("#D2691E"), + Markup.ML_STRING -> get_color("#D2691E"), + Markup.ML_COMMENT -> get_color("#8B0000"), + Markup.ML_MALFORMED -> get_color("#FF6A6A") + ) + val foreground: Markup_Tree.Select[Color] = { - case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => free_color - case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => skolem_color - case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => bound_color + case Text.Info(_, XML.Elem(Markup(m, _), _)) + if foreground_colors.isDefinedAt(m) => foreground_colors(m) } val tooltip: Markup_Tree.Select[String] = @@ -162,39 +186,6 @@ { import Token._ Map[String, Byte]( - // logical entities - Markup.TCLASS -> NULL, - Markup.TYCON -> NULL, - Markup.FIXED -> NULL, - Markup.CONST -> LITERAL2, - Markup.DYNAMIC_FACT -> LABEL, - // inner syntax - Markup.TFREE -> NULL, - Markup.FREE -> NULL, - Markup.TVAR -> NULL, - Markup.SKOLEM -> NULL, - Markup.BOUND -> NULL, - Markup.VAR -> NULL, - Markup.NUM -> DIGIT, - Markup.FLOAT -> DIGIT, - Markup.XNUM -> DIGIT, - Markup.XSTR -> LITERAL4, - Markup.LITERAL -> OPERATOR, - Markup.INNER_COMMENT -> COMMENT1, - Markup.SORT -> NULL, - Markup.TYP -> NULL, - Markup.TERM -> NULL, - Markup.PROP -> NULL, - // ML syntax - Markup.ML_KEYWORD -> KEYWORD1, - Markup.ML_DELIMITER -> OPERATOR, - Markup.ML_IDENT -> NULL, - Markup.ML_TVAR -> NULL, - Markup.ML_NUMERAL -> DIGIT, - Markup.ML_CHAR -> LITERAL1, - Markup.ML_STRING -> LITERAL1, - Markup.ML_COMMENT -> COMMENT1, - Markup.ML_MALFORMED -> INVALID, // embedded source text Markup.ML_SOURCE -> COMMENT3, Markup.DOC_SOURCE -> COMMENT3, diff -r 9cd4b4ecb4dd -r 328dcc5cc43f 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 15:58:01 2011 +0200 @@ -0,0 +1,284 @@ +/* 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.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.{TextAreaExtension, TextAreaPainter} + + +class Text_Area_Painter(doc_view: Document_View) +{ + private val model = doc_view.model + private val buffer = model.buffer + 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(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 def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] = + { + val painter = text_area.getPainter + val font = painter.getFont + val font_context = painter.getFontRenderContext + + // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged + // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength + val margin = + if (buffer.getStringProperty("wrap") != "soft") 0.0f + 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 + }.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, 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 + } + + private def paint_chunk_list(gfx: Graphics2D, + offset: Text.Offset, head: Chunk, x: Float, y: Float): Float = + { + val clip_rect = gfx.getClipBounds + val font_context = text_area.getPainter.getFontRenderContext + + var w = 0.0f + var chunk_offset = 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(chunk_offset, chunk_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 x1 = x + w + for (Text.Info(range, info) <- markup) { + val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset) + gfx.setColor(info.getOrElse(chunk_color)) + gfx.drawString(str, x1.toInt, y.toInt) + x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat + } + } + } + w += chunk.width + chunk_offset += chunk_length + chunk = chunk.next.asInstanceOf[Chunk] + } + w + } + + 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) + { + Isabelle.swing_buffer_lock(buffer) { + val clip = gfx.getClip + val x0 = text_area.getHorizontalOffset + val fm = text_area.getPainter.getFontMetrics + var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent + + val infos = line_infos(physical_lines.iterator.filter(i => i != -1)) + for (i <- 0 until physical_lines.length) { + if (physical_lines(i) != -1) { + infos.get(start(i)) match { + case Some(chunk) => + val w = paint_chunk_list(gfx, 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 + 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 9cd4b4ecb4dd -r 328dcc5cc43f src/Tools/jEdit/src/text_painter.scala --- a/src/Tools/jEdit/src/text_painter.scala Tue Jun 14 13:50:54 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) - } -} -