diff --git a/src/Tools/jEdit/src/text_area_painter.scala b/src/Tools/jEdit/src/text_area_painter.scala --- a/src/Tools/jEdit/src/text_area_painter.scala +++ b/src/Tools/jEdit/src/text_area_painter.scala @@ -1,396 +1,410 @@ /* 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, Shape} import java.awt.font.TextAttribute import java.text.AttributedString 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, JEditTextArea} 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 /* original painters */ private def pick_extension(name: String): TextAreaExtension = { text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList match { case List(x) => x case _ => error("Expected exactly one " + name) } } private val orig_text_painter = pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText") /* common painter state */ @volatile private var painter_snapshot: Document.Snapshot = null @volatile private var painter_clip: Shape = null private val set_state = 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) { doc_view.robust_body(()) { painter_snapshot = doc_view.update_snapshot() painter_clip = gfx.getClip } } } private val reset_state = 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) { doc_view.robust_body(()) { painter_snapshot = null painter_clip = null } } } /* 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) { doc_view.robust_body(()) { 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 for { (command, command_start) <- snapshot.node.command_range(snapshot.revert(line_range)) if !command.is_ignored range <- line_range.try_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) } // 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 */ def char_width(): Int = { val painter = text_area.getPainter val font = painter.getFont val font_context = painter.getFontRenderContext font.getStringBounds(" ", font_context).getWidth.round.toInt } 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 - char_width() * 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, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float = { val clip_rect = gfx.getClipBounds val painter = text_area.getPainter val font_context = painter.getFontRenderContext var w = 0.0f var chunk = head while (chunk != null) { val chunk_offset = line_start + chunk.offset if (x + w + chunk.width > clip_rect.x && x + w < clip_rect.x + clip_rect.width && chunk.accessable) { val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length) val chunk_font = chunk.style.getFont val chunk_color = chunk.style.getForegroundColor + def string_width(s: String): Float = + if (s.isEmpty) 0.0f + else chunk_font.getStringBounds(s, font_context).getWidth.toFloat + val caret_range = if (text_area.hasFocus) doc_view.caret_range() else Text.Range(-1) val markup = for { r1 <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color) r2 <- r1.try_restrict(chunk_range) } yield r2 val padded_markup = if (markup.isEmpty) Iterator(Text.Info(chunk_range, None)) else Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++ markup.iterator ++ Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None)) var x1 = x + w gfx.setFont(chunk_font) for (Text.Info(range, info) <- padded_markup if !range.is_singularity) { val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset) gfx.setColor(info.getOrElse(chunk_color)) range.try_restrict(caret_range) match { case Some(r) if !r.is_singularity => - val astr = new AttributedString(str) val i = r.start - range.start val j = r.stop - range.start + val s1 = str.substring(0, i) + val s2 = str.substring(i, j) + val s3 = str.substring(j) + + if (!s1.isEmpty) gfx.drawString(s1, x1, y) + + val astr = new AttributedString(s2) astr.addAttribute(TextAttribute.FONT, chunk_font) - astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j) - astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j) - gfx.drawString(astr.getIterator, x1, y) + astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor) + astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON) + gfx.drawString(astr.getIterator, x1 + string_width(s1), y) + + if (!s3.isEmpty) + gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y) + case _ => gfx.drawString(str, x1, y) } - x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat + x1 += string_width(str) } } w += chunk.width 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) { doc_view.robust_body(()) { 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) { val x1 = infos.get(start(i)) match { case None => x0 case Some(chunk) => gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height) val w = paint_chunk_list(gfx, start(i), chunk, x0, y0).toInt x0 + w.toInt } gfx.clipRect(x1, 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) } y0 += line_height } } } } /* foreground */ private val foreground_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) { doc_view.robust_body(()) { val snapshot = painter_snapshot for (i <- 0 until physical_lines.length) { if (physical_lines(i) != -1) { val line_range = doc_view.proper_line_range(start(i), end(i)) // highlighted range -- 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.fillRect(r.x, y + i * line_height, r.length, line_height) } case _ => } } } } } } /* caret -- outside of text range */ private class Caret_Painter(before: Boolean) extends TextAreaExtension { override def paintValidLine(gfx: Graphics2D, screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) { doc_view.robust_body(()) { if (before) gfx.clipRect(0, 0, 0, 0) else gfx.setClip(painter_clip) } } } private val before_caret_painter1 = new Caret_Painter(true) private val after_caret_painter1 = new Caret_Painter(false) private val before_caret_painter2 = new Caret_Painter(true) private val after_caret_painter2 = new Caret_Painter(false) private val caret_painter = new TextAreaExtension { override def paintValidLine(gfx: Graphics2D, screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) { doc_view.robust_body(()) { if (text_area.hasFocus) { val caret = text_area.getCaretPosition if (start <= caret && caret == end - 1) { val painter = text_area.getPainter val fm = painter.getFontMetrics val offset = caret - text_area.getLineStartOffset(physical_line) val x = text_area.offsetToXY(physical_line, offset).x gfx.setColor(painter.getCaretColor) gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1) } } } } } /* activation */ def activate() { val painter = text_area.getPainter painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state) painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter) painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1) painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1) painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2) painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2) painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter) painter.addExtension(500, foreground_painter) painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state) painter.removeExtension(orig_text_painter) } def deactivate() { val painter = text_area.getPainter painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) painter.removeExtension(reset_state) painter.removeExtension(foreground_painter) painter.removeExtension(caret_painter) painter.removeExtension(after_caret_painter2) painter.removeExtension(before_caret_painter2) painter.removeExtension(after_caret_painter1) painter.removeExtension(before_caret_painter1) painter.removeExtension(text_painter) painter.removeExtension(background_painter) painter.removeExtension(set_state) } }