1.1 --- a/src/Tools/jEdit/src/text_painter.scala Mon Jun 13 12:29:26 2011 +0200
1.2 +++ b/src/Tools/jEdit/src/text_painter.scala Mon Jun 13 12:33:53 2011 +0200
1.3 @@ -29,77 +29,70 @@
1.4 }
1.5 }
1.6
1.7 - var use = false
1.8 -
1.9 override def paintScreenLineRange(gfx: Graphics2D,
1.10 first_line: Int, last_line: Int, physical_lines: Array[Int],
1.11 start: Array[Int], end: Array[Int], y: Int, line_height: Int)
1.12 {
1.13 - if (use) {
1.14 - val buffer = text_area.getBuffer
1.15 - Isabelle.swing_buffer_lock(buffer) {
1.16 - val painter = text_area.getPainter
1.17 - val font = painter.getFont
1.18 - val font_context = painter.getFontRenderContext
1.19 - val fm = painter.getFontMetrics
1.20 + val buffer = text_area.getBuffer
1.21 + Isabelle.swing_buffer_lock(buffer) {
1.22 + val painter = text_area.getPainter
1.23 + val font = painter.getFont
1.24 + val font_context = painter.getFontRenderContext
1.25 + val fm = painter.getFontMetrics
1.26
1.27 - // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
1.28 - // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
1.29 - val char_width = font.getStringBounds(" ", font_context).getWidth.round.toInt
1.30 - val soft_wrap = buffer.getStringProperty("wrap") == "soft"
1.31 - val wrap_margin =
1.32 - {
1.33 - val max = buffer.getIntegerProperty("maxLineLen", 0)
1.34 - if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
1.35 - else if (soft_wrap) painter.getWidth - char_width * 3
1.36 - else 0
1.37 - }.toFloat
1.38 + // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
1.39 + // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
1.40 + val char_width = font.getStringBounds(" ", font_context).getWidth.round.toInt
1.41 + val soft_wrap = buffer.getStringProperty("wrap") == "soft"
1.42 + val wrap_margin =
1.43 + {
1.44 + val max = buffer.getIntegerProperty("maxLineLen", 0)
1.45 + if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
1.46 + else if (soft_wrap) painter.getWidth - char_width * 3
1.47 + else 0
1.48 + }.toFloat
1.49
1.50 - val line_infos: Map[Text.Offset, Chunk] =
1.51 - {
1.52 - val out = new ArrayList[Chunk]
1.53 - val handler = new DisplayTokenHandler
1.54 - val margin = if (soft_wrap) wrap_margin else 0.0f
1.55 + val line_infos: Map[Text.Offset, Chunk] =
1.56 + {
1.57 + val out = new ArrayList[Chunk]
1.58 + val handler = new DisplayTokenHandler
1.59 + val margin = if (soft_wrap) wrap_margin else 0.0f
1.60
1.61 - var result = Map[Text.Offset, Chunk]()
1.62 - for (line <- physical_lines.iterator.filter(i => i != -1)) {
1.63 - out.clear
1.64 - handler.init(painter.getStyles, font_context, painter, out, margin)
1.65 - buffer.markTokens(line, handler)
1.66 + var result = Map[Text.Offset, Chunk]()
1.67 + for (line <- physical_lines.iterator.filter(i => i != -1)) {
1.68 + out.clear
1.69 + handler.init(painter.getStyles, font_context, painter, out, margin)
1.70 + buffer.markTokens(line, handler)
1.71
1.72 - val line_start = buffer.getLineStartOffset(line)
1.73 - for (i <- 0 until out.size) {
1.74 - val chunk = out.get(i)
1.75 - result += (line_start + chunk.offset -> chunk)
1.76 - }
1.77 + val line_start = buffer.getLineStartOffset(line)
1.78 + for (i <- 0 until out.size) {
1.79 + val chunk = out.get(i)
1.80 + result += (line_start + chunk.offset -> chunk)
1.81 }
1.82 - result
1.83 }
1.84 + result
1.85 + }
1.86
1.87 - val clip = gfx.getClip
1.88 - val x0 = text_area.getHorizontalOffset
1.89 - var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
1.90 - for (i <- 0 until physical_lines.length) {
1.91 - if (physical_lines(i) != -1) {
1.92 - line_infos.get(start(i)) match {
1.93 - case Some(chunk) =>
1.94 - val w = Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR).toInt
1.95 - gfx.setFont(font)
1.96 - gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
1.97 - orig_text_painter.paintValidLine(
1.98 - gfx, first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
1.99 - gfx.setClip(clip)
1.100 + val clip = gfx.getClip
1.101 + val x0 = text_area.getHorizontalOffset
1.102 + var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
1.103 + for (i <- 0 until physical_lines.length) {
1.104 + if (physical_lines(i) != -1) {
1.105 + line_infos.get(start(i)) match {
1.106 + case Some(chunk) =>
1.107 + val w = Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR).toInt
1.108 + gfx.setFont(font)
1.109 + gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
1.110 + orig_text_painter.paintValidLine(
1.111 + gfx, first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
1.112 + gfx.setClip(clip)
1.113
1.114 - case None =>
1.115 - }
1.116 + case None =>
1.117 }
1.118 - y0 += line_height
1.119 }
1.120 + y0 += line_height
1.121 }
1.122 }
1.123 - else
1.124 - orig_text_painter.paintScreenLineRange(
1.125 - gfx, first_line, last_line, physical_lines, start, end, y, line_height)
1.126 }
1.127
1.128