--- a/src/Tools/jEdit/src/text_area_painter.scala Tue Jun 14 11:36:08 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala Tue Jun 14 12:18:34 2011 +0200
@@ -20,6 +20,7 @@
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 =
@@ -72,7 +73,7 @@
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) {
+ Isabelle.swing_buffer_lock(buffer) {
val snapshot = painter_snapshot()
val ascent = text_area.getPainter.getFontMetrics.getAscent
@@ -147,110 +148,107 @@
/* 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 xpos = 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, xpos.toInt, y.toInt)
+ xpos += 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_start: Int, line_height: Int)
+ start: Array[Int], end: Array[Int], y: 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
+ 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) {
- line_infos.get(start(i)) match {
+ infos.get(start(i)) match {
case Some(chunk) =>
- val w = paint_chunk_list(start(i), chunk, x0, y0).toInt
+ 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_start + line_height * i)
+ first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
gfx.setClip(clip)
-
case None =>
}
}