src/Tools/jEdit/src/rich_text_area.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23 ago)
changeset 57612 990ffb84489b
parent 56884 7de69b35bdaf
child 57857 4d86378e635f
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
     1 /*  Title:      Tools/jEdit/src/rich_text_area.scala
     2     Author:     Makarius
     3 
     4 Enhanced version of jEdit text area, with rich text rendering,
     5 tooltips, hyperlinks etc.
     6 */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import isabelle._
    12 
    13 import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor, MouseInfo}
    14 import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
    15   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
    16 import java.awt.font.TextAttribute
    17 import javax.swing.SwingUtilities
    18 import java.text.AttributedString
    19 import java.util.ArrayList
    20 
    21 import scala.util.matching.Regex
    22 
    23 import org.gjt.sp.util.Log
    24 import org.gjt.sp.jedit.{OperatingSystem, Debug, View}
    25 import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
    26 import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}
    27 
    28 
    29 class Rich_Text_Area(
    30   view: View,
    31   text_area: TextArea,
    32   get_rendering: () => Rendering,
    33   close_action: () => Unit,
    34   get_search_pattern: () => Option[Regex],
    35   caret_visible: Boolean,
    36   enable_hovering: Boolean)
    37 {
    38   private val buffer = text_area.getBuffer
    39 
    40 
    41   /* robust extension body */
    42 
    43   def robust_body[A](default: A)(body: => A): A =
    44   {
    45     try {
    46       GUI_Thread.require {}
    47       if (buffer == text_area.getBuffer) body
    48       else {
    49         Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
    50         default
    51       }
    52     }
    53     catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); default }
    54   }
    55 
    56 
    57   /* original painters */
    58 
    59   private def pick_extension(name: String): TextAreaExtension =
    60   {
    61     text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
    62     match {
    63       case List(x) => x
    64       case _ => error("Expected exactly one " + name)
    65     }
    66   }
    67 
    68   private val orig_text_painter =
    69     pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
    70 
    71 
    72   /* common painter state */
    73 
    74   @volatile private var painter_rendering: Rendering = null
    75   @volatile private var painter_clip: Shape = null
    76 
    77   private val set_state = new TextAreaExtension
    78   {
    79     override def paintScreenLineRange(gfx: Graphics2D,
    80       first_line: Int, last_line: Int, physical_lines: Array[Int],
    81       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    82     {
    83       painter_rendering = get_rendering()
    84       painter_clip = gfx.getClip
    85     }
    86   }
    87 
    88   private val reset_state = new TextAreaExtension
    89   {
    90     override def paintScreenLineRange(gfx: Graphics2D,
    91       first_line: Int, last_line: Int, physical_lines: Array[Int],
    92       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    93     {
    94       painter_rendering = null
    95       painter_clip = null
    96     }
    97   }
    98 
    99   def robust_rendering(body: Rendering => Unit)
   100   {
   101     robust_body(()) { body(painter_rendering) }
   102   }
   103 
   104 
   105   /* active areas within the text */
   106 
   107   private class Active_Area[A](
   108     rendering: Rendering => Text.Range => Option[Text.Info[A]],
   109     cursor: Option[Int])
   110   {
   111     private var the_text_info: Option[(String, Text.Info[A])] = None
   112 
   113     def is_active: Boolean = the_text_info.isDefined
   114     def text_info: Option[(String, Text.Info[A])] = the_text_info
   115     def info: Option[Text.Info[A]] = the_text_info.map(_._2)
   116 
   117     def update(new_info: Option[Text.Info[A]])
   118     {
   119       val old_text_info = the_text_info
   120       val new_text_info =
   121         new_info.map(info => (text_area.getText(info.range.start, info.range.length), info))
   122 
   123       if (new_text_info != old_text_info) {
   124         if (cursor.isDefined) {
   125           if (new_text_info.isDefined)
   126             text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get))
   127           else
   128             text_area.getPainter.resetCursor()
   129         }
   130         for {
   131           r0 <- JEdit_Lib.visible_range(text_area)
   132           opt <- List(old_text_info, new_text_info)
   133           (_, Text.Info(r1, _)) <- opt
   134           r2 <- r1.try_restrict(r0)  // FIXME more precise?!
   135         } JEdit_Lib.invalidate_range(text_area, r2)
   136         the_text_info = new_text_info
   137       }
   138     }
   139 
   140     def update_rendering(r: Rendering, range: Text.Range)
   141     { update(rendering(r)(range)) }
   142 
   143     def reset { update(None) }
   144   }
   145 
   146   // owned by GUI thread
   147 
   148   private val highlight_area =
   149     new Active_Area[Color]((r: Rendering) => r.highlight _, None)
   150   private val hyperlink_area =
   151     new Active_Area[PIDE.editor.Hyperlink](
   152       (r: Rendering) => r.hyperlink _, Some(Cursor.HAND_CURSOR))
   153   private val active_area =
   154     new Active_Area[XML.Elem]((r: Rendering) => r.active _, Some(Cursor.DEFAULT_CURSOR))
   155 
   156   private val active_areas =
   157     List((highlight_area, true), (hyperlink_area, true), (active_area, false))
   158   def active_reset(): Unit = active_areas.foreach(_._1.reset)
   159 
   160   private val focus_listener = new FocusAdapter {
   161     override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
   162   }
   163 
   164   private val window_listener = new WindowAdapter {
   165     override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } }
   166     override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } }
   167   }
   168 
   169   private val mouse_listener = new MouseAdapter {
   170     override def mouseClicked(e: MouseEvent) {
   171       robust_body(()) {
   172         hyperlink_area.info match {
   173           case Some(Text.Info(range, link)) =>
   174             if (!link.external) {
   175               try { text_area.moveCaretPosition(range.start) }
   176               catch {
   177                 case _: ArrayIndexOutOfBoundsException =>
   178                 case _: IllegalArgumentException =>
   179               }
   180               text_area.requestFocus
   181             }
   182             link.follow(view)
   183           case None =>
   184         }
   185         active_area.text_info match {
   186           case Some((text, Text.Info(_, markup))) =>
   187             Active.action(view, text, markup)
   188             close_action()
   189           case None =>
   190         }
   191       }
   192     }
   193   }
   194 
   195   private def mouse_inside_painter(): Boolean =
   196     MouseInfo.getPointerInfo match {
   197       case null => false
   198       case info =>
   199         val point = info.getLocation
   200         val painter = text_area.getPainter
   201         SwingUtilities.convertPointFromScreen(point, painter)
   202         painter.contains(point)
   203     }
   204 
   205   private val mouse_motion_listener = new MouseMotionAdapter {
   206     override def mouseDragged(evt: MouseEvent) {
   207       robust_body(()) {
   208         Completion_Popup.Text_Area.dismissed(text_area)
   209         Pretty_Tooltip.dismiss_descendant(text_area.getPainter)
   210       }
   211     }
   212 
   213     override def mouseMoved(evt: MouseEvent) {
   214       robust_body(()) {
   215         val x = evt.getX
   216         val y = evt.getY
   217         val control = (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
   218 
   219         if ((control || enable_hovering) && !buffer.isLoading) {
   220           JEdit_Lib.buffer_lock(buffer) {
   221             JEdit_Lib.pixel_range(text_area, x, y) match {
   222               case None => active_reset()
   223               case Some(range) =>
   224                 val rendering = get_rendering()
   225                 for ((area, require_control) <- active_areas)
   226                 {
   227                   if (control == require_control && !rendering.snapshot.is_outdated)
   228                     area.update_rendering(rendering, range)
   229                   else area.reset
   230                 }
   231             }
   232           }
   233         }
   234         else active_reset()
   235 
   236         if (evt.getSource == text_area.getPainter) {
   237           Pretty_Tooltip.invoke(() =>
   238             robust_body(()) {
   239               if (mouse_inside_painter()) {
   240                 val rendering = get_rendering()
   241                 val snapshot = rendering.snapshot
   242                 if (!snapshot.is_outdated) {
   243                   JEdit_Lib.pixel_range(text_area, x, y) match {
   244                     case None =>
   245                     case Some(range) =>
   246                       val result =
   247                         if (control) rendering.tooltip(range)
   248                         else rendering.tooltip_message(range)
   249                       result match {
   250                         case None =>
   251                         case Some(tip) =>
   252                           val painter = text_area.getPainter
   253                           val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2)
   254                           val results = rendering.command_results(tip.range)
   255                           Pretty_Tooltip(view, painter, loc, rendering, results, tip)
   256                       }
   257                   }
   258                 }
   259               }
   260           })
   261         }
   262       }
   263     }
   264   }
   265 
   266 
   267   /* text background */
   268 
   269   private val background_painter = new TextAreaExtension
   270   {
   271     override def paintScreenLineRange(gfx: Graphics2D,
   272       first_line: Int, last_line: Int, physical_lines: Array[Int],
   273       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   274     {
   275       robust_rendering { rendering =>
   276         val fm = text_area.getPainter.getFontMetrics
   277 
   278         for (i <- 0 until physical_lines.length) {
   279           if (physical_lines(i) != -1) {
   280             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
   281 
   282             // line background color
   283             for { (color, separator) <- rendering.line_background(line_range) }
   284             {
   285               gfx.setColor(color)
   286               val sep = if (separator) (2 min (line_height / 2)) else 0
   287               gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
   288             }
   289 
   290             // background color
   291             for {
   292               Text.Info(range, color) <- rendering.background(line_range)
   293               r <- JEdit_Lib.gfx_range(text_area, range)
   294             } {
   295               gfx.setColor(color)
   296               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   297             }
   298 
   299             // active area -- potentially from other snapshot
   300             for {
   301               info <- active_area.info
   302               Text.Info(range, _) <- info.try_restrict(line_range)
   303               r <- JEdit_Lib.gfx_range(text_area, range)
   304             } {
   305               gfx.setColor(rendering.active_hover_color)
   306               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   307             }
   308 
   309             // squiggly underline
   310             for {
   311               Text.Info(range, color) <- rendering.squiggly_underline(line_range)
   312               r <- JEdit_Lib.gfx_range(text_area, range)
   313             } {
   314               gfx.setColor(color)
   315               val x0 = (r.x / 2) * 2
   316               val y0 = r.y + fm.getAscent + 1
   317               for (x1 <- Range(x0, x0 + r.length, 2)) {
   318                 val y1 = if (x1 % 4 < 2) y0 else y0 + 1
   319                 gfx.drawLine(x1, y1, x1 + 1, y1)
   320               }
   321             }
   322 
   323             // spell checker
   324             for {
   325               spell_checker <- PIDE.spell_checker.get
   326               spell_range <- rendering.spell_checker_ranges(line_range)
   327               text <- JEdit_Lib.try_get_text(buffer, spell_range)
   328               info <- spell_checker.marked_words(spell_range.start, text)
   329               r <- JEdit_Lib.gfx_range(text_area, info.range)
   330             } {
   331               gfx.setColor(rendering.spell_checker_color)
   332               val y0 = r.y + ((fm.getAscent + 4) min (line_height - 2))
   333               gfx.drawLine(r.x, y0, r.x + r.length, y0)
   334             }
   335           }
   336         }
   337       }
   338     }
   339   }
   340 
   341 
   342   /* text */
   343 
   344   private def caret_enabled: Boolean =
   345     caret_visible && (!text_area.hasFocus || text_area.isCaretVisible)
   346 
   347   private def caret_color(rendering: Rendering): Color =
   348   {
   349     if (text_area.isCaretVisible)
   350       text_area.getPainter.getCaretColor
   351     else rendering.caret_invisible_color
   352   }
   353 
   354   private def paint_chunk_list(rendering: Rendering,
   355     gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   356   {
   357     val clip_rect = gfx.getClipBounds
   358     val painter = text_area.getPainter
   359     val font_context = painter.getFontRenderContext
   360 
   361     val caret_range =
   362       if (caret_enabled) JEdit_Lib.caret_range(text_area)
   363       else Text.Range.offside
   364 
   365     var w = 0.0f
   366     var chunk = head
   367     while (chunk != null) {
   368       val chunk_offset = line_start + chunk.offset
   369       if (x + w + chunk.width > clip_rect.x &&
   370           x + w < clip_rect.x + clip_rect.width && chunk.length > 0)
   371       {
   372         val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
   373         val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
   374         val chunk_font = chunk.style.getFont
   375         val chunk_color = chunk.style.getForegroundColor
   376 
   377         def string_width(s: String): Float =
   378           if (s.isEmpty) 0.0f
   379           else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
   380 
   381         val markup =
   382           for {
   383             r1 <- rendering.text_color(chunk_range, chunk_color)
   384             r2 <- r1.try_restrict(chunk_range)
   385           } yield r2
   386 
   387         val padded_markup_iterator =
   388           if (markup.isEmpty)
   389             Iterator(Text.Info(chunk_range, chunk_color))
   390           else
   391             Iterator(
   392               Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
   393             markup.iterator ++
   394             Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
   395 
   396         var x1 = x + w
   397         gfx.setFont(chunk_font)
   398         for (Text.Info(range, color) <- padded_markup_iterator if !range.is_singularity) {
   399           val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
   400           gfx.setColor(color)
   401 
   402           range.try_restrict(caret_range) match {
   403             case Some(r) if !r.is_singularity =>
   404               val i = r.start - range.start
   405               val j = r.stop - range.start
   406               val s1 = str.substring(0, i)
   407               val s2 = str.substring(i, j)
   408               val s3 = str.substring(j)
   409 
   410               if (!s1.isEmpty) gfx.drawString(s1, x1, y)
   411 
   412               val astr = new AttributedString(s2)
   413               astr.addAttribute(TextAttribute.FONT, chunk_font)
   414               astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering))
   415               astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
   416               gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
   417 
   418               if (!s3.isEmpty)
   419                 gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
   420 
   421             case _ =>
   422               gfx.drawString(str, x1, y)
   423           }
   424           x1 += string_width(str)
   425         }
   426       }
   427       w += chunk.width
   428       chunk = chunk.next.asInstanceOf[Chunk]
   429     }
   430     w
   431   }
   432 
   433   private val text_painter = new TextAreaExtension
   434   {
   435     override def paintScreenLineRange(gfx: Graphics2D,
   436       first_line: Int, last_line: Int, physical_lines: Array[Int],
   437       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   438     {
   439       robust_rendering { rendering =>
   440         val painter = text_area.getPainter
   441         val fm = painter.getFontMetrics
   442         val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext)
   443 
   444         val clip = gfx.getClip
   445         val x0 = text_area.getHorizontalOffset
   446         var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
   447 
   448         val (bullet_x, bullet_y, bullet_w, bullet_h) =
   449         {
   450           val w = fm.charWidth(' ')
   451           val b = (w / 2) max 1
   452           val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt
   453           ((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
   454         }
   455 
   456         for (i <- 0 until physical_lines.length) {
   457           val line = physical_lines(i)
   458           if (line != -1) {
   459             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
   460 
   461             // bullet bar
   462             for {
   463               Text.Info(range, color) <- rendering.bullet(line_range)
   464               r <- JEdit_Lib.gfx_range(text_area, range)
   465             } {
   466               gfx.setColor(color)
   467               gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y,
   468                 r.length - bullet_w, line_height - bullet_h)
   469             }
   470 
   471             // text chunks
   472             val screen_line = first_line + i
   473             val chunks = text_area.getChunksOfScreenLine(screen_line)
   474             if (chunks != null) {
   475               try {
   476                 val line_start = buffer.getLineStartOffset(line)
   477                 gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
   478                 val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
   479                 gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   480                 orig_text_painter.paintValidLine(gfx,
   481                   screen_line, line, start(i), end(i), y + line_height * i)
   482               } finally { gfx.setClip(clip) }
   483             }
   484           }
   485           y0 += line_height
   486         }
   487       }
   488     }
   489   }
   490 
   491 
   492   /* foreground */
   493 
   494   private val foreground_painter = new TextAreaExtension
   495   {
   496     override def paintScreenLineRange(gfx: Graphics2D,
   497       first_line: Int, last_line: Int, physical_lines: Array[Int],
   498       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   499     {
   500       robust_rendering { rendering =>
   501         val search_pattern = get_search_pattern()
   502         for (i <- 0 until physical_lines.length) {
   503           if (physical_lines(i) != -1) {
   504             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
   505 
   506             // foreground color
   507             for {
   508               Text.Info(range, color) <- rendering.foreground(line_range)
   509               r <- JEdit_Lib.gfx_range(text_area, range)
   510             } {
   511               gfx.setColor(color)
   512               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   513             }
   514 
   515             // search pattern
   516             for {
   517               regex <- search_pattern
   518               text <- JEdit_Lib.try_get_text(buffer, line_range)
   519               m <- regex.findAllMatchIn(text)
   520               range = Text.Range(m.start, m.end) + line_range.start
   521               r <- JEdit_Lib.gfx_range(text_area, range)
   522             } {
   523               gfx.setColor(rendering.search_color)
   524               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   525             }
   526 
   527             // highlight range -- potentially from other snapshot
   528             for {
   529               info <- highlight_area.info
   530               Text.Info(range, color) <- info.try_restrict(line_range)
   531               r <- JEdit_Lib.gfx_range(text_area, range)
   532             } {
   533               gfx.setColor(color)
   534               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   535             }
   536 
   537             // hyperlink range -- potentially from other snapshot
   538             for {
   539               info <- hyperlink_area.info
   540               Text.Info(range, _) <- info.try_restrict(line_range)
   541               r <- JEdit_Lib.gfx_range(text_area, range)
   542             } {
   543               gfx.setColor(rendering.hyperlink_color)
   544               gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
   545             }
   546 
   547             // completion range
   548             if (!hyperlink_area.is_active && caret_visible) {
   549               for {
   550                 completion <- Completion_Popup.Text_Area(text_area)
   551                 Text.Info(range, color) <- completion.rendering(rendering, line_range)
   552                 r <- JEdit_Lib.gfx_range(text_area, range)
   553               } {
   554                 gfx.setColor(color)
   555                 gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
   556               }
   557             }
   558           }
   559         }
   560       }
   561     }
   562   }
   563 
   564 
   565   /* caret -- outside of text range */
   566 
   567   private class Caret_Painter(before: Boolean) extends TextAreaExtension
   568   {
   569     override def paintValidLine(gfx: Graphics2D,
   570       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   571     {
   572       robust_rendering { _ =>
   573         if (before) gfx.clipRect(0, 0, 0, 0)
   574         else gfx.setClip(painter_clip)
   575       }
   576     }
   577   }
   578 
   579   private val before_caret_painter1 = new Caret_Painter(true)
   580   private val after_caret_painter1 = new Caret_Painter(false)
   581   private val before_caret_painter2 = new Caret_Painter(true)
   582   private val after_caret_painter2 = new Caret_Painter(false)
   583 
   584   private val caret_painter = new TextAreaExtension
   585   {
   586     override def paintValidLine(gfx: Graphics2D,
   587       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   588     {
   589       robust_rendering { rendering =>
   590         if (caret_visible) {
   591           val caret = text_area.getCaretPosition
   592           if (caret_enabled && start <= caret && caret == end - 1) {
   593             val painter = text_area.getPainter
   594             val fm = painter.getFontMetrics
   595 
   596             val offset = caret - text_area.getLineStartOffset(physical_line)
   597             val x = text_area.offsetToXY(physical_line, offset).x
   598             val y1 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
   599 
   600             val astr = new AttributedString(" ")
   601             astr.addAttribute(TextAttribute.FONT, painter.getFont)
   602             astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering))
   603             astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
   604 
   605             val clip = gfx.getClip
   606             try {
   607               gfx.clipRect(x, y, Integer.MAX_VALUE, painter.getLineHeight)
   608               gfx.drawString(astr.getIterator, x, y1)
   609             }
   610             finally { gfx.setClip(clip) }
   611           }
   612         }
   613       }
   614     }
   615   }
   616 
   617 
   618   /* activation */
   619 
   620   def activate()
   621   {
   622     val painter = text_area.getPainter
   623     painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
   624     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   625     painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
   626     painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
   627     painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
   628     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
   629     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
   630     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
   631     painter.addExtension(500, foreground_painter)
   632     painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
   633     painter.removeExtension(orig_text_painter)
   634     painter.addMouseListener(mouse_listener)
   635     painter.addMouseMotionListener(mouse_motion_listener)
   636     text_area.addFocusListener(focus_listener)
   637     view.addWindowListener(window_listener)
   638   }
   639 
   640   def deactivate()
   641   {
   642     active_reset()
   643     val painter = text_area.getPainter
   644     view.removeWindowListener(window_listener)
   645     text_area.removeFocusListener(focus_listener)
   646     painter.removeMouseMotionListener(mouse_motion_listener)
   647     painter.removeMouseListener(mouse_listener)
   648     painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   649     painter.removeExtension(reset_state)
   650     painter.removeExtension(foreground_painter)
   651     painter.removeExtension(caret_painter)
   652     painter.removeExtension(after_caret_painter2)
   653     painter.removeExtension(before_caret_painter2)
   654     painter.removeExtension(after_caret_painter1)
   655     painter.removeExtension(before_caret_painter1)
   656     painter.removeExtension(text_painter)
   657     painter.removeExtension(background_painter)
   658     painter.removeExtension(set_state)
   659   }
   660 }
   661