src/Tools/jEdit/src/text_area_painter.scala
author wenzelm
Tue Jun 14 11:36:08 2011 +0200 (2011-06-14)
changeset 43381 806878ae2219
parent 43376 src/Tools/jEdit/src/text_painter.scala@0f6880c1c759
child 43382 5d9d34bdec25
permissions -rw-r--r--
separate module for text area painting;
wenzelm@43381
     1
/*  Title:      Tools/jEdit/src/text_area_painter.scala
wenzelm@43369
     2
    Author:     Makarius
wenzelm@43369
     3
wenzelm@43381
     4
Painter setup for main jEdit text area.
wenzelm@43369
     5
*/
wenzelm@43369
     6
wenzelm@43369
     7
package isabelle.jedit
wenzelm@43369
     8
wenzelm@43369
     9
wenzelm@43369
    10
import isabelle._
wenzelm@43369
    11
wenzelm@43369
    12
import java.awt.{Graphics, Graphics2D}
wenzelm@43369
    13
import java.util.ArrayList
wenzelm@43369
    14
wenzelm@43369
    15
import org.gjt.sp.jedit.Debug
wenzelm@43369
    16
import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
wenzelm@43369
    17
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
wenzelm@43369
    18
wenzelm@43369
    19
wenzelm@43381
    20
class Text_Area_Painter(doc_view: Document_View)
wenzelm@43369
    21
{
wenzelm@43381
    22
  private val model = doc_view.model
wenzelm@43376
    23
  private val text_area = doc_view.text_area
wenzelm@43376
    24
wenzelm@43369
    25
  private val orig_text_painter: TextAreaExtension =
wenzelm@43369
    26
  {
wenzelm@43369
    27
    val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText"
wenzelm@43369
    28
    text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
wenzelm@43369
    29
    match {
wenzelm@43369
    30
      case List(x) => x
wenzelm@43369
    31
      case _ => error("Expected exactly one " + name)
wenzelm@43369
    32
    }
wenzelm@43369
    33
  }
wenzelm@43369
    34
wenzelm@43381
    35
wenzelm@43381
    36
  /* painter snapshot */
wenzelm@43381
    37
wenzelm@43381
    38
  @volatile private var _painter_snapshot: Option[Document.Snapshot] = None
wenzelm@43381
    39
wenzelm@43381
    40
  private def painter_snapshot(): Document.Snapshot =
wenzelm@43381
    41
    _painter_snapshot match {
wenzelm@43381
    42
      case Some(snapshot) => snapshot
wenzelm@43381
    43
      case None => error("Missing document snapshot for text area painter")
wenzelm@43381
    44
    }
wenzelm@43381
    45
wenzelm@43381
    46
  private val set_snapshot = new TextAreaExtension
wenzelm@43381
    47
  {
wenzelm@43381
    48
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
    49
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381
    50
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
    51
    {
wenzelm@43381
    52
      _painter_snapshot = Some(model.snapshot())
wenzelm@43381
    53
    }
wenzelm@43381
    54
  }
wenzelm@43381
    55
wenzelm@43381
    56
  private val reset_snapshot = new TextAreaExtension
wenzelm@43369
    57
  {
wenzelm@43381
    58
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
    59
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381
    60
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
    61
    {
wenzelm@43381
    62
      _painter_snapshot = None
wenzelm@43381
    63
    }
wenzelm@43381
    64
  }
wenzelm@43381
    65
wenzelm@43381
    66
wenzelm@43381
    67
  /* text background */
wenzelm@43376
    68
wenzelm@43381
    69
  private val background_painter = new TextAreaExtension
wenzelm@43381
    70
  {
wenzelm@43381
    71
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
    72
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381
    73
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
    74
    {
wenzelm@43381
    75
      Isabelle.swing_buffer_lock(model.buffer) {
wenzelm@43381
    76
        val snapshot = painter_snapshot()
wenzelm@43381
    77
        val ascent = text_area.getPainter.getFontMetrics.getAscent
wenzelm@43376
    78
wenzelm@43381
    79
        for (i <- 0 until physical_lines.length) {
wenzelm@43381
    80
          if (physical_lines(i) != -1) {
wenzelm@43381
    81
            val line_range = doc_view.proper_line_range(start(i), end(i))
wenzelm@43376
    82
wenzelm@43381
    83
            // background color: status
wenzelm@43381
    84
            val cmds = snapshot.node.command_range(snapshot.revert(line_range))
wenzelm@43381
    85
            for {
wenzelm@43381
    86
              (command, command_start) <- cmds if !command.is_ignored
wenzelm@43381
    87
              val range = line_range.restrict(snapshot.convert(command.range + command_start))
wenzelm@43381
    88
              r <- Isabelle.gfx_range(text_area, range)
wenzelm@43381
    89
              color <- Isabelle_Markup.status_color(snapshot, command)
wenzelm@43381
    90
            } {
wenzelm@43381
    91
              gfx.setColor(color)
wenzelm@43381
    92
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@43381
    93
            }
wenzelm@43376
    94
wenzelm@43381
    95
            // background color (1): markup
wenzelm@43381
    96
            for {
wenzelm@43381
    97
              Text.Info(range, Some(color)) <-
wenzelm@43381
    98
                snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
wenzelm@43381
    99
              r <- Isabelle.gfx_range(text_area, range)
wenzelm@43381
   100
            } {
wenzelm@43381
   101
              gfx.setColor(color)
wenzelm@43381
   102
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@43381
   103
            }
wenzelm@43376
   104
wenzelm@43381
   105
            // background color (2): markup
wenzelm@43381
   106
            for {
wenzelm@43381
   107
              Text.Info(range, Some(color)) <-
wenzelm@43381
   108
                snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
wenzelm@43381
   109
              r <- Isabelle.gfx_range(text_area, range)
wenzelm@43381
   110
            } {
wenzelm@43381
   111
              gfx.setColor(color)
wenzelm@43381
   112
              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
wenzelm@43376
   113
            }
wenzelm@43381
   114
wenzelm@43381
   115
            // sub-expression highlighting -- potentially from other snapshot
wenzelm@43381
   116
            doc_view.highlight_range match {
wenzelm@43381
   117
              case Some((range, color)) if line_range.overlaps(range) =>
wenzelm@43381
   118
                Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
wenzelm@43381
   119
                  case None =>
wenzelm@43381
   120
                  case Some(r) =>
wenzelm@43381
   121
                    gfx.setColor(color)
wenzelm@43381
   122
                    gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
wenzelm@43381
   123
                }
wenzelm@43381
   124
              case _ =>
wenzelm@43381
   125
            }
wenzelm@43381
   126
wenzelm@43381
   127
            // squiggly underline
wenzelm@43381
   128
            for {
wenzelm@43381
   129
              Text.Info(range, Some(color)) <-
wenzelm@43381
   130
                snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
wenzelm@43381
   131
              r <- Isabelle.gfx_range(text_area, range)
wenzelm@43381
   132
            } {
wenzelm@43381
   133
              gfx.setColor(color)
wenzelm@43381
   134
              val x0 = (r.x / 2) * 2
wenzelm@43381
   135
              val y0 = r.y + ascent + 1
wenzelm@43381
   136
              for (x1 <- Range(x0, x0 + r.length, 2)) {
wenzelm@43381
   137
                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
wenzelm@43381
   138
                gfx.drawLine(x1, y1, x1 + 1, y1)
wenzelm@43376
   139
              }
wenzelm@43376
   140
            }
wenzelm@43376
   141
          }
wenzelm@43376
   142
        }
wenzelm@43376
   143
      }
wenzelm@43381
   144
    }
wenzelm@43381
   145
  }
wenzelm@43381
   146
wenzelm@43381
   147
wenzelm@43381
   148
  /* text */
wenzelm@43369
   149
wenzelm@43381
   150
  private val text_painter = new TextAreaExtension
wenzelm@43381
   151
  {
wenzelm@43381
   152
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
   153
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381
   154
      start: Array[Int], end: Array[Int], y_start: Int, line_height: Int)
wenzelm@43381
   155
    {
wenzelm@43381
   156
      val buffer = text_area.getBuffer
wenzelm@43381
   157
      Isabelle.swing_buffer_lock(buffer) {
wenzelm@43381
   158
        val painter = text_area.getPainter
wenzelm@43381
   159
        val font = painter.getFont
wenzelm@43381
   160
        val font_context = painter.getFontRenderContext
wenzelm@43381
   161
        val font_metrics = painter.getFontMetrics
wenzelm@43371
   162
wenzelm@43381
   163
        def paint_chunk_list(head_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
wenzelm@43381
   164
        {
wenzelm@43381
   165
          val clip_rect = gfx.getClipBounds
wenzelm@43381
   166
wenzelm@43381
   167
          var w = 0.0f
wenzelm@43381
   168
          var offset = head_offset
wenzelm@43381
   169
          var chunk = head
wenzelm@43381
   170
          while (chunk != null) {
wenzelm@43381
   171
            val chunk_length = if (chunk.str == null) 0 else chunk.str.length
wenzelm@43381
   172
wenzelm@43381
   173
            if (x + w + chunk.width > clip_rect.x &&
wenzelm@43381
   174
                x + w < clip_rect.x + clip_rect.width &&
wenzelm@43381
   175
                chunk.accessable && chunk.visible)
wenzelm@43381
   176
            {
wenzelm@43381
   177
              val chunk_range = Text.Range(offset, offset + chunk_length)
wenzelm@43381
   178
              val chunk_font = chunk.style.getFont
wenzelm@43381
   179
              val chunk_color = chunk.style.getForegroundColor
wenzelm@43381
   180
wenzelm@43381
   181
              val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
wenzelm@43371
   182
wenzelm@43381
   183
              gfx.setFont(chunk_font)
wenzelm@43381
   184
              if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
wenzelm@43381
   185
                  markup.forall(info => info.info.isEmpty)) {
wenzelm@43381
   186
                gfx.setColor(chunk_color)
wenzelm@43381
   187
                gfx.drawGlyphVector(chunk.gv, x + w, y)
wenzelm@43381
   188
              }
wenzelm@43381
   189
              else {
wenzelm@43381
   190
                var xpos = x + w
wenzelm@43381
   191
                for (Text.Info(range, info) <- markup) {
wenzelm@43381
   192
                  val str = chunk.str.substring(range.start - offset, range.stop - offset)
wenzelm@43381
   193
                  gfx.setColor(info.getOrElse(chunk_color))
wenzelm@43381
   194
                  gfx.drawString(str, xpos.toInt, y.toInt)
wenzelm@43381
   195
                  xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
wenzelm@43381
   196
                }
wenzelm@43381
   197
              }
wenzelm@43381
   198
            }
wenzelm@43381
   199
            w += chunk.width
wenzelm@43381
   200
            offset += chunk_length
wenzelm@43381
   201
            chunk = chunk.next.asInstanceOf[Chunk]
wenzelm@43381
   202
          }
wenzelm@43381
   203
          w
wenzelm@43381
   204
        }
wenzelm@43371
   205
wenzelm@43381
   206
        // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
wenzelm@43381
   207
        // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
wenzelm@43381
   208
        val char_width = font.getStringBounds(" ", font_context).getWidth.round.toInt
wenzelm@43381
   209
        val soft_wrap = buffer.getStringProperty("wrap") == "soft"
wenzelm@43381
   210
        val wrap_margin =
wenzelm@43381
   211
        {
wenzelm@43381
   212
          val max = buffer.getIntegerProperty("maxLineLen", 0)
wenzelm@43381
   213
          if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
wenzelm@43381
   214
          else if (soft_wrap) painter.getWidth - char_width * 3
wenzelm@43381
   215
          else 0
wenzelm@43381
   216
        }.toFloat
wenzelm@43369
   217
wenzelm@43381
   218
        val line_infos: Map[Text.Offset, Chunk] =
wenzelm@43381
   219
        {
wenzelm@43381
   220
          val out = new ArrayList[Chunk]
wenzelm@43381
   221
          val handler = new DisplayTokenHandler
wenzelm@43381
   222
          val margin = if (soft_wrap) wrap_margin else 0.0f
wenzelm@43381
   223
wenzelm@43381
   224
          var result = Map[Text.Offset, Chunk]()
wenzelm@43381
   225
          for (line <- physical_lines.iterator.filter(i => i != -1)) {
wenzelm@43381
   226
            out.clear
wenzelm@43381
   227
            handler.init(painter.getStyles, font_context, painter, out, margin)
wenzelm@43381
   228
            buffer.markTokens(line, handler)
wenzelm@43381
   229
wenzelm@43381
   230
            val line_start = buffer.getLineStartOffset(line)
wenzelm@43381
   231
            for (i <- 0 until out.size) {
wenzelm@43381
   232
              val chunk = out.get(i)
wenzelm@43381
   233
              result += (line_start + chunk.offset -> chunk)
wenzelm@43381
   234
            }
wenzelm@43381
   235
          }
wenzelm@43381
   236
          result
wenzelm@43381
   237
        }
wenzelm@43376
   238
wenzelm@43381
   239
        val clip = gfx.getClip
wenzelm@43381
   240
        val x0 = text_area.getHorizontalOffset
wenzelm@43381
   241
        var y0 =
wenzelm@43381
   242
          y_start + font_metrics.getHeight - (font_metrics.getLeading + 1) - font_metrics.getDescent
wenzelm@43372
   243
wenzelm@43381
   244
        for (i <- 0 until physical_lines.length) {
wenzelm@43381
   245
          if (physical_lines(i) != -1) {
wenzelm@43381
   246
            line_infos.get(start(i)) match {
wenzelm@43381
   247
              case Some(chunk) =>
wenzelm@43381
   248
                val w = paint_chunk_list(start(i), chunk, x0, y0).toInt
wenzelm@43381
   249
                gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
wenzelm@43381
   250
                orig_text_painter.paintValidLine(gfx,
wenzelm@43381
   251
                  first_line + i, physical_lines(i), start(i), end(i), y_start + line_height * i)
wenzelm@43381
   252
                gfx.setClip(clip)
wenzelm@43381
   253
wenzelm@43381
   254
              case None =>
wenzelm@43381
   255
            }
wenzelm@43369
   256
          }
wenzelm@43381
   257
          y0 += line_height
wenzelm@43369
   258
        }
wenzelm@43369
   259
      }
wenzelm@43369
   260
    }
wenzelm@43369
   261
  }
wenzelm@43369
   262
wenzelm@43369
   263
wenzelm@43369
   264
  /* activation */
wenzelm@43369
   265
wenzelm@43369
   266
  def activate()
wenzelm@43369
   267
  {
wenzelm@43369
   268
    val painter = text_area.getPainter
wenzelm@43381
   269
    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
wenzelm@43381
   270
    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
wenzelm@43381
   271
    painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
wenzelm@43381
   272
    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
wenzelm@43369
   273
    painter.removeExtension(orig_text_painter)
wenzelm@43369
   274
  }
wenzelm@43369
   275
wenzelm@43369
   276
  def deactivate()
wenzelm@43369
   277
  {
wenzelm@43369
   278
    val painter = text_area.getPainter
wenzelm@43369
   279
    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
wenzelm@43381
   280
    painter.removeExtension(reset_snapshot)
wenzelm@43381
   281
    painter.removeExtension(text_painter)
wenzelm@43381
   282
    painter.removeExtension(background_painter)
wenzelm@43381
   283
    painter.removeExtension(set_snapshot)
wenzelm@43369
   284
  }
wenzelm@43369
   285
}
wenzelm@43369
   286