diff -r 806878ae2219 -r 5d9d34bdec25 src/Tools/jEdit/src/text_area_painter.scala --- 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 => } }