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