src/Tools/jEdit/src/text_area_painter.scala
changeset 43382 5d9d34bdec25
parent 43381 806878ae2219
child 43383 63fc6b5ef8ac
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Tue Jun 14 11:36:08 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Tue Jun 14 12:18:34 2011 +0200
     1.3 @@ -20,6 +20,7 @@
     1.4  class Text_Area_Painter(doc_view: Document_View)
     1.5  {
     1.6    private val model = doc_view.model
     1.7 +  private val buffer = model.buffer
     1.8    private val text_area = doc_view.text_area
     1.9  
    1.10    private val orig_text_painter: TextAreaExtension =
    1.11 @@ -72,7 +73,7 @@
    1.12        first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.13        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.14      {
    1.15 -      Isabelle.swing_buffer_lock(model.buffer) {
    1.16 +      Isabelle.swing_buffer_lock(buffer) {
    1.17          val snapshot = painter_snapshot()
    1.18          val ascent = text_area.getPainter.getFontMetrics.getAscent
    1.19  
    1.20 @@ -147,110 +148,107 @@
    1.21  
    1.22    /* text */
    1.23  
    1.24 +  private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
    1.25 +  {
    1.26 +    val painter = text_area.getPainter
    1.27 +    val font = painter.getFont
    1.28 +    val font_context = painter.getFontRenderContext
    1.29 +
    1.30 +    // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
    1.31 +    // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
    1.32 +    val margin =
    1.33 +      if (buffer.getStringProperty("wrap") != "soft") 0.0f
    1.34 +      else {
    1.35 +        val max = buffer.getIntegerProperty("maxLineLen", 0)
    1.36 +        if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
    1.37 +        else painter.getWidth - font.getStringBounds(" ", font_context).getWidth.round.toInt * 3
    1.38 +      }.toFloat
    1.39 +
    1.40 +    val out = new ArrayList[Chunk]
    1.41 +    val handler = new DisplayTokenHandler
    1.42 +
    1.43 +    var result = Map[Text.Offset, Chunk]()
    1.44 +    for (line <- physical_lines) {
    1.45 +      out.clear
    1.46 +      handler.init(painter.getStyles, font_context, painter, out, margin)
    1.47 +      buffer.markTokens(line, handler)
    1.48 +
    1.49 +      val line_start = buffer.getLineStartOffset(line)
    1.50 +      for (i <- 0 until out.size) {
    1.51 +        val chunk = out.get(i)
    1.52 +        result += (line_start + chunk.offset -> chunk)
    1.53 +      }
    1.54 +    }
    1.55 +    result
    1.56 +  }
    1.57 +
    1.58 +  private def paint_chunk_list(gfx: Graphics2D,
    1.59 +    offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
    1.60 +  {
    1.61 +    val clip_rect = gfx.getClipBounds
    1.62 +    val font_context = text_area.getPainter.getFontRenderContext
    1.63 +
    1.64 +    var w = 0.0f
    1.65 +    var chunk_offset = offset
    1.66 +    var chunk = head
    1.67 +    while (chunk != null) {
    1.68 +      val chunk_length = if (chunk.str == null) 0 else chunk.str.length
    1.69 +
    1.70 +      if (x + w + chunk.width > clip_rect.x &&
    1.71 +          x + w < clip_rect.x + clip_rect.width &&
    1.72 +          chunk.accessable && chunk.visible)
    1.73 +      {
    1.74 +        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk_length)
    1.75 +        val chunk_font = chunk.style.getFont
    1.76 +        val chunk_color = chunk.style.getForegroundColor
    1.77 +
    1.78 +        val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
    1.79 +
    1.80 +        gfx.setFont(chunk_font)
    1.81 +        if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
    1.82 +            markup.forall(info => info.info.isEmpty)) {
    1.83 +          gfx.setColor(chunk_color)
    1.84 +          gfx.drawGlyphVector(chunk.gv, x + w, y)
    1.85 +        }
    1.86 +        else {
    1.87 +          var xpos = x + w
    1.88 +          for (Text.Info(range, info) <- markup) {
    1.89 +            val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
    1.90 +            gfx.setColor(info.getOrElse(chunk_color))
    1.91 +            gfx.drawString(str, xpos.toInt, y.toInt)
    1.92 +            xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
    1.93 +          }
    1.94 +        }
    1.95 +      }
    1.96 +      w += chunk.width
    1.97 +      chunk_offset += chunk_length
    1.98 +      chunk = chunk.next.asInstanceOf[Chunk]
    1.99 +    }
   1.100 +    w
   1.101 +  }
   1.102 +
   1.103    private val text_painter = new TextAreaExtension
   1.104    {
   1.105      override def paintScreenLineRange(gfx: Graphics2D,
   1.106        first_line: Int, last_line: Int, physical_lines: Array[Int],
   1.107 -      start: Array[Int], end: Array[Int], y_start: Int, line_height: Int)
   1.108 +      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   1.109      {
   1.110 -      val buffer = text_area.getBuffer
   1.111        Isabelle.swing_buffer_lock(buffer) {
   1.112 -        val painter = text_area.getPainter
   1.113 -        val font = painter.getFont
   1.114 -        val font_context = painter.getFontRenderContext
   1.115 -        val font_metrics = painter.getFontMetrics
   1.116 -
   1.117 -        def paint_chunk_list(head_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   1.118 -        {
   1.119 -          val clip_rect = gfx.getClipBounds
   1.120 -
   1.121 -          var w = 0.0f
   1.122 -          var offset = head_offset
   1.123 -          var chunk = head
   1.124 -          while (chunk != null) {
   1.125 -            val chunk_length = if (chunk.str == null) 0 else chunk.str.length
   1.126 -
   1.127 -            if (x + w + chunk.width > clip_rect.x &&
   1.128 -                x + w < clip_rect.x + clip_rect.width &&
   1.129 -                chunk.accessable && chunk.visible)
   1.130 -            {
   1.131 -              val chunk_range = Text.Range(offset, offset + chunk_length)
   1.132 -              val chunk_font = chunk.style.getFont
   1.133 -              val chunk_color = chunk.style.getForegroundColor
   1.134 -
   1.135 -              val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
   1.136 -
   1.137 -              gfx.setFont(chunk_font)
   1.138 -              if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
   1.139 -                  markup.forall(info => info.info.isEmpty)) {
   1.140 -                gfx.setColor(chunk_color)
   1.141 -                gfx.drawGlyphVector(chunk.gv, x + w, y)
   1.142 -              }
   1.143 -              else {
   1.144 -                var xpos = x + w
   1.145 -                for (Text.Info(range, info) <- markup) {
   1.146 -                  val str = chunk.str.substring(range.start - offset, range.stop - offset)
   1.147 -                  gfx.setColor(info.getOrElse(chunk_color))
   1.148 -                  gfx.drawString(str, xpos.toInt, y.toInt)
   1.149 -                  xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
   1.150 -                }
   1.151 -              }
   1.152 -            }
   1.153 -            w += chunk.width
   1.154 -            offset += chunk_length
   1.155 -            chunk = chunk.next.asInstanceOf[Chunk]
   1.156 -          }
   1.157 -          w
   1.158 -        }
   1.159 -
   1.160 -        // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
   1.161 -        // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
   1.162 -        val char_width = font.getStringBounds(" ", font_context).getWidth.round.toInt
   1.163 -        val soft_wrap = buffer.getStringProperty("wrap") == "soft"
   1.164 -        val wrap_margin =
   1.165 -        {
   1.166 -          val max = buffer.getIntegerProperty("maxLineLen", 0)
   1.167 -          if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
   1.168 -          else if (soft_wrap) painter.getWidth - char_width * 3
   1.169 -          else 0
   1.170 -        }.toFloat
   1.171 -
   1.172 -        val line_infos: Map[Text.Offset, Chunk] =
   1.173 -        {
   1.174 -          val out = new ArrayList[Chunk]
   1.175 -          val handler = new DisplayTokenHandler
   1.176 -          val margin = if (soft_wrap) wrap_margin else 0.0f
   1.177 -
   1.178 -          var result = Map[Text.Offset, Chunk]()
   1.179 -          for (line <- physical_lines.iterator.filter(i => i != -1)) {
   1.180 -            out.clear
   1.181 -            handler.init(painter.getStyles, font_context, painter, out, margin)
   1.182 -            buffer.markTokens(line, handler)
   1.183 -
   1.184 -            val line_start = buffer.getLineStartOffset(line)
   1.185 -            for (i <- 0 until out.size) {
   1.186 -              val chunk = out.get(i)
   1.187 -              result += (line_start + chunk.offset -> chunk)
   1.188 -            }
   1.189 -          }
   1.190 -          result
   1.191 -        }
   1.192 -
   1.193          val clip = gfx.getClip
   1.194          val x0 = text_area.getHorizontalOffset
   1.195 -        var y0 =
   1.196 -          y_start + font_metrics.getHeight - (font_metrics.getLeading + 1) - font_metrics.getDescent
   1.197 +        val fm = text_area.getPainter.getFontMetrics
   1.198 +        var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
   1.199  
   1.200 +        val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
   1.201          for (i <- 0 until physical_lines.length) {
   1.202            if (physical_lines(i) != -1) {
   1.203 -            line_infos.get(start(i)) match {
   1.204 +            infos.get(start(i)) match {
   1.205                case Some(chunk) =>
   1.206 -                val w = paint_chunk_list(start(i), chunk, x0, y0).toInt
   1.207 +                val w = paint_chunk_list(gfx, start(i), chunk, x0, y0).toInt
   1.208                  gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   1.209                  orig_text_painter.paintValidLine(gfx,
   1.210 -                  first_line + i, physical_lines(i), start(i), end(i), y_start + line_height * i)
   1.211 +                  first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
   1.212                  gfx.setClip(clip)
   1.213 -
   1.214                case None =>
   1.215              }
   1.216            }