src/Tools/jEdit/src/text_area_painter.scala
author wenzelm
Wed Mar 14 15:37:51 2012 +0100 (2012-03-14)
changeset 46920 5f44c8bea84e
parent 46913 3444a24dc4e9
child 47027 fc3bb6c02a3c
permissions -rw-r--r--
more explicit indication of swing thread context;
wenzelm@43381
     1
/*  Title:      Tools/jEdit/src/text_area_painter.scala
wenzelm@43369
     2
    Author:     Makarius
wenzelm@43369
     3
wenzelm@46220
     4
Painter setup for main jEdit text area, depending on common snapshot.
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@43393
    12
import java.awt.{Graphics2D, Shape}
wenzelm@43392
    13
import java.awt.font.TextAttribute
wenzelm@43392
    14
import java.text.AttributedString
wenzelm@43369
    15
import java.util.ArrayList
wenzelm@43369
    16
wenzelm@43369
    17
import org.gjt.sp.jedit.Debug
wenzelm@43369
    18
import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
wenzelm@46224
    19
import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
wenzelm@43369
    20
wenzelm@43369
    21
wenzelm@43381
    22
class Text_Area_Painter(doc_view: Document_View)
wenzelm@43369
    23
{
wenzelm@43381
    24
  private val model = doc_view.model
wenzelm@43382
    25
  private val buffer = model.buffer
wenzelm@43376
    26
  private val text_area = doc_view.text_area
wenzelm@43376
    27
wenzelm@43392
    28
wenzelm@46220
    29
  /* graphics range */
wenzelm@46204
    30
wenzelm@46812
    31
  private def char_width(): Int =
wenzelm@46812
    32
  {
wenzelm@46812
    33
    val painter = text_area.getPainter
wenzelm@46812
    34
    val font = painter.getFont
wenzelm@46812
    35
    val font_context = painter.getFontRenderContext
wenzelm@46812
    36
    font.getStringBounds(" ", font_context).getWidth.round.toInt
wenzelm@46812
    37
  }
wenzelm@46812
    38
wenzelm@46204
    39
  private class Gfx_Range(val x: Int, val y: Int, val length: Int)
wenzelm@46204
    40
wenzelm@46812
    41
  // NB: jEdit already normalizes \r\n and \r to \n
wenzelm@46812
    42
  // NB: last line lacks \n
wenzelm@46204
    43
  private def gfx_range(range: Text.Range): Option[Gfx_Range] =
wenzelm@46204
    44
  {
wenzelm@46204
    45
    val p = text_area.offsetToXY(range.start)
wenzelm@46812
    46
wenzelm@46812
    47
    val end = buffer.getLength
wenzelm@46812
    48
    val stop = range.stop
wenzelm@46812
    49
    val (q, r) =
wenzelm@46812
    50
      if (stop >= end) (text_area.offsetToXY(end), char_width())
wenzelm@46812
    51
      else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
wenzelm@46812
    52
        (text_area.offsetToXY(stop - 1), char_width())
wenzelm@46812
    53
      else (text_area.offsetToXY(stop), 0)
wenzelm@46812
    54
wenzelm@46812
    55
    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
wenzelm@46812
    56
      Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
wenzelm@46204
    57
    else None
wenzelm@46204
    58
  }
wenzelm@46204
    59
wenzelm@46204
    60
wenzelm@43392
    61
  /* original painters */
wenzelm@43392
    62
wenzelm@43392
    63
  private def pick_extension(name: String): TextAreaExtension =
wenzelm@43369
    64
  {
wenzelm@43369
    65
    text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
wenzelm@43369
    66
    match {
wenzelm@43369
    67
      case List(x) => x
wenzelm@43369
    68
      case _ => error("Expected exactly one " + name)
wenzelm@43369
    69
    }
wenzelm@43369
    70
  }
wenzelm@43369
    71
wenzelm@43392
    72
  private val orig_text_painter =
wenzelm@43392
    73
    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
wenzelm@43392
    74
wenzelm@43392
    75
wenzelm@43393
    76
  /* common painter state */
wenzelm@43381
    77
wenzelm@43393
    78
  @volatile private var painter_snapshot: Document.Snapshot = null
wenzelm@43393
    79
  @volatile private var painter_clip: Shape = null
wenzelm@43381
    80
wenzelm@43393
    81
  private val set_state = new TextAreaExtension
wenzelm@43381
    82
  {
wenzelm@43381
    83
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
    84
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381
    85
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
    86
    {
wenzelm@46220
    87
      painter_snapshot = doc_view.update_snapshot()
wenzelm@46220
    88
      painter_clip = gfx.getClip
wenzelm@43381
    89
    }
wenzelm@43381
    90
  }
wenzelm@43381
    91
wenzelm@43393
    92
  private val reset_state = new TextAreaExtension
wenzelm@43369
    93
  {
wenzelm@43381
    94
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
    95
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381
    96
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
    97
    {
wenzelm@46220
    98
      painter_snapshot = null
wenzelm@46220
    99
      painter_clip = null
wenzelm@43381
   100
    }
wenzelm@43381
   101
  }
wenzelm@43381
   102
wenzelm@46220
   103
  private def robust_snapshot(body: Document.Snapshot => Unit)
wenzelm@46220
   104
  {
wenzelm@46220
   105
    doc_view.robust_body(()) { body(painter_snapshot) }
wenzelm@46220
   106
  }
wenzelm@46220
   107
wenzelm@43381
   108
wenzelm@43381
   109
  /* text background */
wenzelm@43376
   110
wenzelm@43381
   111
  private val background_painter = new TextAreaExtension
wenzelm@43381
   112
  {
wenzelm@43381
   113
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
   114
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381
   115
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
   116
    {
wenzelm@46220
   117
      robust_snapshot { snapshot =>
wenzelm@43381
   118
        val ascent = text_area.getPainter.getFontMetrics.getAscent
wenzelm@43376
   119
wenzelm@43381
   120
        for (i <- 0 until physical_lines.length) {
wenzelm@43381
   121
          if (physical_lines(i) != -1) {
wenzelm@43381
   122
            val line_range = doc_view.proper_line_range(start(i), end(i))
wenzelm@43376
   123
wenzelm@46166
   124
            // background color (1)
wenzelm@43381
   125
            for {
wenzelm@46178
   126
              Text.Info(range, color) <- Isabelle_Rendering.background1(snapshot, line_range)
wenzelm@46204
   127
              r <- gfx_range(range)
wenzelm@43381
   128
            } {
wenzelm@43381
   129
              gfx.setColor(color)
wenzelm@43381
   130
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@43381
   131
            }
wenzelm@43376
   132
wenzelm@46166
   133
            // background color (2)
wenzelm@43381
   134
            for {
wenzelm@46178
   135
              Text.Info(range, color) <- Isabelle_Rendering.background2(snapshot, line_range)
wenzelm@46204
   136
              r <- gfx_range(range)
wenzelm@43381
   137
            } {
wenzelm@43381
   138
              gfx.setColor(color)
wenzelm@43381
   139
              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
wenzelm@43376
   140
            }
wenzelm@43381
   141
wenzelm@43381
   142
            // squiggly underline
wenzelm@43381
   143
            for {
wenzelm@46224
   144
              Text.Info(range, color) <- Isabelle_Rendering.squiggly_underline(snapshot, line_range)
wenzelm@46204
   145
              r <- gfx_range(range)
wenzelm@43381
   146
            } {
wenzelm@43381
   147
              gfx.setColor(color)
wenzelm@43381
   148
              val x0 = (r.x / 2) * 2
wenzelm@43381
   149
              val y0 = r.y + ascent + 1
wenzelm@43381
   150
              for (x1 <- Range(x0, x0 + r.length, 2)) {
wenzelm@43381
   151
                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
wenzelm@43381
   152
                gfx.drawLine(x1, y1, x1 + 1, y1)
wenzelm@43376
   153
              }
wenzelm@43376
   154
            }
wenzelm@43376
   155
          }
wenzelm@43376
   156
        }
wenzelm@43376
   157
      }
wenzelm@43381
   158
    }
wenzelm@43381
   159
  }
wenzelm@43381
   160
wenzelm@43381
   161
wenzelm@43381
   162
  /* text */
wenzelm@43369
   163
wenzelm@43382
   164
  private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
wenzelm@43382
   165
  {
wenzelm@43382
   166
    val painter = text_area.getPainter
wenzelm@43382
   167
    val font = painter.getFont
wenzelm@43382
   168
    val font_context = painter.getFontRenderContext
wenzelm@43382
   169
wenzelm@43382
   170
    // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
wenzelm@43382
   171
    // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
wenzelm@43382
   172
    val margin =
wenzelm@43382
   173
      if (buffer.getStringProperty("wrap") != "soft") 0.0f
wenzelm@43382
   174
      else {
wenzelm@43382
   175
        val max = buffer.getIntegerProperty("maxLineLen", 0)
wenzelm@43382
   176
        if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
wenzelm@43393
   177
        else painter.getWidth - char_width() * 3
wenzelm@43382
   178
      }.toFloat
wenzelm@43382
   179
wenzelm@43382
   180
    val out = new ArrayList[Chunk]
wenzelm@43382
   181
    val handler = new DisplayTokenHandler
wenzelm@43382
   182
wenzelm@43382
   183
    var result = Map[Text.Offset, Chunk]()
wenzelm@43382
   184
    for (line <- physical_lines) {
wenzelm@46817
   185
      val line_start = buffer.getLineStartOffset(line)
wenzelm@46817
   186
wenzelm@43382
   187
      out.clear
wenzelm@46913
   188
      handler.init(painter.getStyles, font_context, painter, out, margin, line_start)
wenzelm@43382
   189
      buffer.markTokens(line, handler)
wenzelm@43382
   190
wenzelm@43382
   191
      for (i <- 0 until out.size) {
wenzelm@43382
   192
        val chunk = out.get(i)
wenzelm@43382
   193
        result += (line_start + chunk.offset -> chunk)
wenzelm@43382
   194
      }
wenzelm@43382
   195
    }
wenzelm@43382
   196
    result
wenzelm@43382
   197
  }
wenzelm@43382
   198
wenzelm@46220
   199
  private def paint_chunk_list(snapshot: Document.Snapshot,
wenzelm@43505
   200
    gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
wenzelm@43382
   201
  {
wenzelm@43382
   202
    val clip_rect = gfx.getClipBounds
wenzelm@43392
   203
    val painter = text_area.getPainter
wenzelm@43392
   204
    val font_context = painter.getFontRenderContext
wenzelm@43382
   205
wenzelm@43382
   206
    var w = 0.0f
wenzelm@43382
   207
    var chunk = head
wenzelm@43382
   208
    while (chunk != null) {
wenzelm@43505
   209
      val chunk_offset = line_start + chunk.offset
wenzelm@43382
   210
      if (x + w + chunk.width > clip_rect.x &&
wenzelm@43506
   211
          x + w < clip_rect.x + clip_rect.width && chunk.accessable)
wenzelm@43382
   212
      {
wenzelm@43505
   213
        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
wenzelm@44662
   214
        val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
wenzelm@43382
   215
        val chunk_font = chunk.style.getFont
wenzelm@43382
   216
        val chunk_color = chunk.style.getForegroundColor
wenzelm@43382
   217
wenzelm@44056
   218
        def string_width(s: String): Float =
wenzelm@44056
   219
          if (s.isEmpty) 0.0f
wenzelm@44056
   220
          else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
wenzelm@44056
   221
wenzelm@43448
   222
        val caret_range =
wenzelm@43448
   223
          if (text_area.hasFocus) doc_view.caret_range()
wenzelm@43448
   224
          else Text.Range(-1)
wenzelm@43448
   225
wenzelm@43426
   226
        val markup =
wenzelm@43428
   227
          for {
wenzelm@46220
   228
            r1 <- Isabelle_Rendering.text_color(snapshot, chunk_range, chunk_color)
wenzelm@43450
   229
            r2 <- r1.try_restrict(chunk_range)
wenzelm@43450
   230
          } yield r2
wenzelm@43382
   231
wenzelm@43759
   232
        val padded_markup =
wenzelm@43759
   233
          if (markup.isEmpty)
wenzelm@46197
   234
            Iterator(Text.Info(chunk_range, chunk_color))
wenzelm@43759
   235
          else
wenzelm@46197
   236
            Iterator(
wenzelm@46197
   237
              Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
wenzelm@43759
   238
            markup.iterator ++
wenzelm@46197
   239
            Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
wenzelm@43759
   240
wenzelm@43450
   241
        var x1 = x + w
wenzelm@43382
   242
        gfx.setFont(chunk_font)
wenzelm@46197
   243
        for (Text.Info(range, color) <- padded_markup if !range.is_singularity) {
wenzelm@44662
   244
          val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
wenzelm@46197
   245
          gfx.setColor(color)
wenzelm@43448
   246
wenzelm@43759
   247
          range.try_restrict(caret_range) match {
wenzelm@43759
   248
            case Some(r) if !r.is_singularity =>
wenzelm@43759
   249
              val i = r.start - range.start
wenzelm@43759
   250
              val j = r.stop - range.start
wenzelm@44056
   251
              val s1 = str.substring(0, i)
wenzelm@44056
   252
              val s2 = str.substring(i, j)
wenzelm@44056
   253
              val s3 = str.substring(j)
wenzelm@44056
   254
wenzelm@44056
   255
              if (!s1.isEmpty) gfx.drawString(s1, x1, y)
wenzelm@44056
   256
wenzelm@44056
   257
              val astr = new AttributedString(s2)
wenzelm@43759
   258
              astr.addAttribute(TextAttribute.FONT, chunk_font)
wenzelm@44056
   259
              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
wenzelm@44056
   260
              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
wenzelm@44056
   261
              gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
wenzelm@44056
   262
wenzelm@44056
   263
              if (!s3.isEmpty)
wenzelm@44056
   264
                gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
wenzelm@44056
   265
wenzelm@43759
   266
            case _ =>
wenzelm@43759
   267
              gfx.drawString(str, x1, y)
wenzelm@43382
   268
          }
wenzelm@44056
   269
          x1 += string_width(str)
wenzelm@43382
   270
        }
wenzelm@43382
   271
      }
wenzelm@43382
   272
      w += chunk.width
wenzelm@43382
   273
      chunk = chunk.next.asInstanceOf[Chunk]
wenzelm@43382
   274
    }
wenzelm@43382
   275
    w
wenzelm@43382
   276
  }
wenzelm@43382
   277
wenzelm@43381
   278
  private val text_painter = new TextAreaExtension
wenzelm@43381
   279
  {
wenzelm@43381
   280
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381
   281
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43382
   282
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381
   283
    {
wenzelm@46220
   284
      robust_snapshot { snapshot =>
wenzelm@43381
   285
        val clip = gfx.getClip
wenzelm@43381
   286
        val x0 = text_area.getHorizontalOffset
wenzelm@43382
   287
        val fm = text_area.getPainter.getFontMetrics
wenzelm@43382
   288
        var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
wenzelm@43372
   289
wenzelm@43382
   290
        val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
wenzelm@43381
   291
        for (i <- 0 until physical_lines.length) {
wenzelm@43381
   292
          if (physical_lines(i) != -1) {
wenzelm@43392
   293
            val x1 =
wenzelm@43392
   294
              infos.get(start(i)) match {
wenzelm@43392
   295
                case None => x0
wenzelm@43392
   296
                case Some(chunk) =>
wenzelm@43392
   297
                  gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
wenzelm@46220
   298
                  val w = paint_chunk_list(snapshot, gfx, start(i), chunk, x0, y0).toInt
wenzelm@43392
   299
                  x0 + w.toInt
wenzelm@43392
   300
              }
wenzelm@43392
   301
            gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
wenzelm@43392
   302
            orig_text_painter.paintValidLine(gfx,
wenzelm@43392
   303
              first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
wenzelm@43392
   304
            gfx.setClip(clip)
wenzelm@43369
   305
          }
wenzelm@43381
   306
          y0 += line_height
wenzelm@43369
   307
        }
wenzelm@43369
   308
      }
wenzelm@43369
   309
    }
wenzelm@43369
   310
  }
wenzelm@43369
   311
wenzelm@43369
   312
wenzelm@43435
   313
  /* foreground */
wenzelm@43435
   314
wenzelm@43435
   315
  private val foreground_painter = new TextAreaExtension
wenzelm@43435
   316
  {
wenzelm@43435
   317
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43435
   318
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43435
   319
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43435
   320
    {
wenzelm@46220
   321
      robust_snapshot { snapshot =>
wenzelm@43435
   322
        for (i <- 0 until physical_lines.length) {
wenzelm@43435
   323
          if (physical_lines(i) != -1) {
wenzelm@43435
   324
            val line_range = doc_view.proper_line_range(start(i), end(i))
wenzelm@43435
   325
wenzelm@44545
   326
            // foreground color
wenzelm@44545
   327
            for {
wenzelm@46178
   328
              Text.Info(range, color) <- Isabelle_Rendering.foreground(snapshot, line_range)
wenzelm@46204
   329
              r <- gfx_range(range)
wenzelm@44545
   330
            } {
wenzelm@44545
   331
              gfx.setColor(color)
wenzelm@44545
   332
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@44545
   333
            }
wenzelm@44545
   334
wenzelm@43435
   335
            // highlighted range -- potentially from other snapshot
wenzelm@46205
   336
            for {
wenzelm@46205
   337
              info <- doc_view.highlight_range()
wenzelm@46205
   338
              Text.Info(range, color) <- info.try_restrict(line_range)
wenzelm@46205
   339
              r <- gfx_range(range)
wenzelm@46205
   340
            } {
wenzelm@46205
   341
              gfx.setColor(color)
wenzelm@46205
   342
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@43435
   343
            }
wenzelm@43435
   344
          }
wenzelm@43435
   345
        }
wenzelm@43435
   346
      }
wenzelm@43435
   347
    }
wenzelm@43435
   348
  }
wenzelm@43435
   349
wenzelm@43435
   350
wenzelm@43393
   351
  /* caret -- outside of text range */
wenzelm@43393
   352
wenzelm@43393
   353
  private class Caret_Painter(before: Boolean) extends TextAreaExtension
wenzelm@43393
   354
  {
wenzelm@43393
   355
    override def paintValidLine(gfx: Graphics2D,
wenzelm@43393
   356
      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
wenzelm@43393
   357
    {
wenzelm@46220
   358
      robust_snapshot { _ =>
wenzelm@43404
   359
        if (before) gfx.clipRect(0, 0, 0, 0)
wenzelm@43404
   360
        else gfx.setClip(painter_clip)
wenzelm@43404
   361
      }
wenzelm@43393
   362
    }
wenzelm@43393
   363
  }
wenzelm@43393
   364
wenzelm@43393
   365
  private val before_caret_painter1 = new Caret_Painter(true)
wenzelm@43393
   366
  private val after_caret_painter1 = new Caret_Painter(false)
wenzelm@43393
   367
  private val before_caret_painter2 = new Caret_Painter(true)
wenzelm@43393
   368
  private val after_caret_painter2 = new Caret_Painter(false)
wenzelm@43393
   369
wenzelm@43393
   370
  private val caret_painter = new TextAreaExtension
wenzelm@43393
   371
  {
wenzelm@43393
   372
    override def paintValidLine(gfx: Graphics2D,
wenzelm@43393
   373
      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
wenzelm@43393
   374
    {
wenzelm@46220
   375
      robust_snapshot { _ =>
wenzelm@43398
   376
        if (text_area.hasFocus) {
wenzelm@43398
   377
          val caret = text_area.getCaretPosition
wenzelm@43398
   378
          if (start <= caret && caret == end - 1) {
wenzelm@43398
   379
            val painter = text_area.getPainter
wenzelm@43398
   380
            val fm = painter.getFontMetrics
wenzelm@43393
   381
wenzelm@43398
   382
            val offset = caret - text_area.getLineStartOffset(physical_line)
wenzelm@43398
   383
            val x = text_area.offsetToXY(physical_line, offset).x
wenzelm@43398
   384
            gfx.setColor(painter.getCaretColor)
wenzelm@43398
   385
            gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1)
wenzelm@43398
   386
          }
wenzelm@43393
   387
        }
wenzelm@43393
   388
      }
wenzelm@43393
   389
    }
wenzelm@43393
   390
  }
wenzelm@43393
   391
wenzelm@43393
   392
wenzelm@43369
   393
  /* activation */
wenzelm@43369
   394
wenzelm@43369
   395
  def activate()
wenzelm@43369
   396
  {
wenzelm@43369
   397
    val painter = text_area.getPainter
wenzelm@43393
   398
    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
wenzelm@43381
   399
    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
wenzelm@43381
   400
    painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
wenzelm@43393
   401
    painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
wenzelm@43393
   402
    painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
wenzelm@43393
   403
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
wenzelm@43393
   404
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
wenzelm@43393
   405
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
wenzelm@43435
   406
    painter.addExtension(500, foreground_painter)
wenzelm@43393
   407
    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
wenzelm@43369
   408
    painter.removeExtension(orig_text_painter)
wenzelm@43369
   409
  }
wenzelm@43369
   410
wenzelm@43369
   411
  def deactivate()
wenzelm@43369
   412
  {
wenzelm@43369
   413
    val painter = text_area.getPainter
wenzelm@43396
   414
    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
wenzelm@43393
   415
    painter.removeExtension(reset_state)
wenzelm@43435
   416
    painter.removeExtension(foreground_painter)
wenzelm@43393
   417
    painter.removeExtension(caret_painter)
wenzelm@43393
   418
    painter.removeExtension(after_caret_painter2)
wenzelm@43393
   419
    painter.removeExtension(before_caret_painter2)
wenzelm@43393
   420
    painter.removeExtension(after_caret_painter1)
wenzelm@43393
   421
    painter.removeExtension(before_caret_painter1)
wenzelm@43381
   422
    painter.removeExtension(text_painter)
wenzelm@43381
   423
    painter.removeExtension(background_painter)
wenzelm@43393
   424
    painter.removeExtension(set_state)
wenzelm@43369
   425
  }
wenzelm@43369
   426
}
wenzelm@43369
   427