# HG changeset patch # User wenzelm # Date 1307999341 -7200 # Node ID 0f6880c1c759dceadda9bb021b3de96e84b6cdf3 # Parent 09d992ab57c65b944a64b8b3f0163c85e54b9a47 some direct text foreground painting, instead of token marking; common snapshot for all text area painters (NOT gutter etc.) tuned; diff -r 09d992ab57c6 -r 0f6880c1c759 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Mon Jun 13 14:22:33 2011 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Mon Jun 13 23:09:01 2011 +0200 @@ -62,7 +62,7 @@ } -class Document_View(val model: Document_Model, text_area: JEditTextArea) +class Document_View(val model: Document_Model, val text_area: JEditTextArea) { private val session = model.session @@ -207,7 +207,35 @@ } - /* TextArea painters */ + /* 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 { @@ -216,7 +244,7 @@ start: Array[Int], end: Array[Int], y: Int, line_height: Int) { Isabelle.swing_buffer_lock(model.buffer) { - val snapshot = model.snapshot() + val snapshot = text_area_snapshot() val ascent = text_area.getPainter.getFontMetrics.getAscent for (i <- 0 until physical_lines.length) { @@ -310,7 +338,10 @@ } } - val text_painter = new Text_Painter(model, text_area) + val text_painter = new Text_Painter(this) + + + /* Gutter painting */ private val gutter_painter = new TextAreaExtension { @@ -480,8 +511,12 @@ 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) + text_area.getGutter.addExtension(gutter_painter) text_area.addFocusListener(focus_listener) text_area.getView.addWindowListener(window_listener) @@ -495,6 +530,7 @@ private def deactivate() { val painter = text_area.getPainter + session.commands_changed -= main_actor session.global_settings -= main_actor text_area.removeFocusListener(focus_listener) @@ -503,8 +539,11 @@ 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) exit_popup() } } diff -r 09d992ab57c6 -r 0f6880c1c759 src/Tools/jEdit/src/isabelle_markup.scala --- a/src/Tools/jEdit/src/isabelle_markup.scala Mon Jun 13 14:22:33 2011 +0200 +++ b/src/Tools/jEdit/src/isabelle_markup.scala Mon Jun 13 23:09:01 2011 +0200 @@ -28,6 +28,10 @@ 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, 0x8B, 0) + class Icon(val priority: Int, val icon: javax.swing.Icon) { def >= (that: Icon): Boolean = this.priority >= that.priority @@ -100,6 +104,13 @@ case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color } + 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 + } + val tooltip: Markup_Tree.Select[String] = { case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\"" @@ -157,10 +168,10 @@ Markup.DYNAMIC_FACT -> LABEL, // inner syntax Markup.TFREE -> NULL, - Markup.FREE -> MARKUP, + Markup.FREE -> NULL, Markup.TVAR -> NULL, - Markup.SKOLEM -> COMMENT2, - Markup.BOUND -> LABEL, + Markup.SKOLEM -> NULL, + Markup.BOUND -> NULL, Markup.VAR -> NULL, Markup.NUM -> DIGIT, Markup.FLOAT -> DIGIT, diff -r 09d992ab57c6 -r 0f6880c1c759 src/Tools/jEdit/src/text_painter.scala --- a/src/Tools/jEdit/src/text_painter.scala Mon Jun 13 14:22:33 2011 +0200 +++ b/src/Tools/jEdit/src/text_painter.scala Mon Jun 13 23:09:01 2011 +0200 @@ -17,8 +17,10 @@ import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter} -class Text_Painter(model: Document_Model, text_area: JEditTextArea) extends TextAreaExtension +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" @@ -33,35 +35,56 @@ first_line: Int, last_line: Int, physical_lines: Array[Int], start: Array[Int], end: Array[Int], y_start: Int, line_height: Int) { - def paint_chunk_list(head: Chunk, x: Float, y: Float): Float = - { - val clip_rect = gfx.getClipBounds - var w = 0.0f - var chunk = head - while (chunk != null) { - if (x + w + chunk.width > clip_rect.x && - x + w < clip_rect.x + clip_rect.width && - chunk.accessable && chunk.visible) - { - gfx.setFont(chunk.style.getFont) - gfx.setColor(chunk.style.getForegroundColor) - if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null) - gfx.drawGlyphVector(chunk.gv, x + w, y) - else if (chunk.str != null) - gfx.drawString(chunk.str, (x + w).toInt, y.toInt) - } - w += chunk.width - chunk = chunk.next.asInstanceOf[Chunk] - } - w - } - 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 fm = painter.getFontMetrics + 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 @@ -98,12 +121,14 @@ val clip = gfx.getClip val x0 = text_area.getHorizontalOffset - var y0 = y_start + fm.getHeight - (fm.getLeading + 1) - fm.getDescent + 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(chunk, x0, y0).toInt + 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)