src/Tools/jEdit/src/rich_text_area.scala
author wenzelm
Thu Apr 14 22:55:53 2016 +0200 (2016-04-14)
changeset 62986 9d2fae6b31cc
parent 62812 ce22e5c3d4ce
child 62988 224e8d8a4fb8
permissions -rw-r--r--
background color for entity def/ref focus;
     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](
   150       (rendering: Rendering) => rendering.highlight _, None)
   151 
   152   private val hyperlink_area =
   153     new Active_Area[PIDE.editor.Hyperlink](
   154       (rendering: Rendering) => rendering.hyperlink _, Some(Cursor.HAND_CURSOR))
   155 
   156   private val active_area =
   157     new Active_Area[XML.Elem](
   158       (rendering: Rendering) => rendering.active _, Some(Cursor.DEFAULT_CURSOR))
   159 
   160   private val active_areas =
   161     List((highlight_area, true), (hyperlink_area, true), (active_area, false))
   162   def active_reset(): Unit = active_areas.foreach(_._1.reset)
   163 
   164   private val focus_listener = new FocusAdapter {
   165     override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
   166   }
   167 
   168   private val window_listener = new WindowAdapter {
   169     override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } }
   170     override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } }
   171   }
   172 
   173   private val mouse_listener = new MouseAdapter {
   174     override def mouseClicked(e: MouseEvent) {
   175       robust_body(()) {
   176         hyperlink_area.info match {
   177           case Some(Text.Info(range, link)) =>
   178             if (!link.external) {
   179               try { text_area.moveCaretPosition(range.start) }
   180               catch {
   181                 case _: ArrayIndexOutOfBoundsException =>
   182                 case _: IllegalArgumentException =>
   183               }
   184               text_area.requestFocus
   185             }
   186             link.follow(view)
   187           case None =>
   188         }
   189         active_area.text_info match {
   190           case Some((text, Text.Info(_, markup))) =>
   191             Active.action(view, text, markup)
   192             close_action()
   193           case None =>
   194         }
   195       }
   196     }
   197   }
   198 
   199   private def mouse_inside_painter(): Boolean =
   200     MouseInfo.getPointerInfo match {
   201       case null => false
   202       case info =>
   203         val point = info.getLocation
   204         val painter = text_area.getPainter
   205         SwingUtilities.convertPointFromScreen(point, painter)
   206         painter.contains(point)
   207     }
   208 
   209   private val mouse_motion_listener = new MouseMotionAdapter {
   210     override def mouseDragged(evt: MouseEvent) {
   211       robust_body(()) {
   212         active_reset()
   213         Completion_Popup.Text_Area.dismissed(text_area)
   214         Pretty_Tooltip.dismiss_descendant(text_area.getPainter)
   215       }
   216     }
   217 
   218     override def mouseMoved(evt: MouseEvent) {
   219       robust_body(()) {
   220         val x = evt.getX
   221         val y = evt.getY
   222         val control = (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
   223 
   224         if ((control || enable_hovering) && !buffer.isLoading) {
   225           JEdit_Lib.buffer_lock(buffer) {
   226             JEdit_Lib.pixel_range(text_area, x, y) match {
   227               case None => active_reset()
   228               case Some(range) =>
   229                 val rendering = get_rendering()
   230                 for ((area, require_control) <- active_areas)
   231                 {
   232                   if (control == require_control && !rendering.snapshot.is_outdated)
   233                     area.update_rendering(rendering, range)
   234                   else area.reset
   235                 }
   236             }
   237           }
   238         }
   239         else active_reset()
   240 
   241         if (evt.getSource == text_area.getPainter) {
   242           Pretty_Tooltip.invoke(() =>
   243             robust_body(()) {
   244               if (mouse_inside_painter()) {
   245                 val rendering = get_rendering()
   246                 val snapshot = rendering.snapshot
   247                 if (!snapshot.is_outdated) {
   248                   JEdit_Lib.pixel_range(text_area, x, y) match {
   249                     case None =>
   250                     case Some(range) =>
   251                       val result =
   252                         if (control) rendering.tooltip(range)
   253                         else rendering.tooltip_message(range)
   254                       result match {
   255                         case None =>
   256                         case Some(tip) =>
   257                           val painter = text_area.getPainter
   258                           val loc = new Point(x, y + painter.getLineHeight / 2)
   259                           val results = rendering.command_results(tip.range)
   260                           Pretty_Tooltip(view, painter, loc, rendering, results, tip)
   261                       }
   262                   }
   263                 }
   264               }
   265           })
   266         }
   267       }
   268     }
   269   }
   270 
   271 
   272   /* text background */
   273 
   274   private val background_painter = new TextAreaExtension
   275   {
   276     override def paintScreenLineRange(gfx: Graphics2D,
   277       first_line: Int, last_line: Int, physical_lines: Array[Int],
   278       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   279     {
   280       robust_rendering { rendering =>
   281         val fm = text_area.getPainter.getFontMetrics
   282 
   283         val focus =
   284           JEdit_Lib.visible_range(text_area) match {
   285             case Some(visible_range) if caret_enabled =>
   286               rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range)
   287             case _ => Set.empty[Long]
   288           }
   289 
   290         for (i <- 0 until physical_lines.length) {
   291           if (physical_lines(i) != -1) {
   292             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
   293 
   294             // line background color
   295             for { (color, separator) <- rendering.line_background(line_range) }
   296             {
   297               gfx.setColor(color)
   298               val sep = if (separator) 2 min (line_height / 2) else 0
   299               gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
   300             }
   301 
   302             // background color
   303             for {
   304               Text.Info(range, color) <- rendering.background(line_range, focus)
   305               r <- JEdit_Lib.gfx_range(text_area, range)
   306             } {
   307               gfx.setColor(color)
   308               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   309             }
   310 
   311             // active area -- potentially from other snapshot
   312             for {
   313               info <- active_area.info
   314               Text.Info(range, _) <- info.try_restrict(line_range)
   315               r <- JEdit_Lib.gfx_range(text_area, range)
   316             } {
   317               gfx.setColor(rendering.active_hover_color)
   318               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   319             }
   320 
   321             // squiggly underline
   322             for {
   323               Text.Info(range, color) <- rendering.squiggly_underline(line_range)
   324               r <- JEdit_Lib.gfx_range(text_area, range)
   325             } {
   326               gfx.setColor(color)
   327               val x0 = (r.x / 2) * 2
   328               val y0 = r.y + fm.getAscent + 1
   329               for (x1 <- Range(x0, x0 + r.length, 2)) {
   330                 val y1 = if (x1 % 4 < 2) y0 else y0 + 1
   331                 gfx.drawLine(x1, y1, x1 + 1, y1)
   332               }
   333             }
   334 
   335             // spell checker
   336             for {
   337               spell_checker <- PIDE.spell_checker.get
   338               spell_range <- rendering.spell_checker_ranges(line_range)
   339               text <- JEdit_Lib.try_get_text(buffer, spell_range)
   340               info <- spell_checker.marked_words(spell_range.start, text)
   341               r <- JEdit_Lib.gfx_range(text_area, info.range)
   342             } {
   343               gfx.setColor(rendering.spell_checker_color)
   344               val y0 = r.y + ((fm.getAscent + 4) min (line_height - 2))
   345               gfx.drawLine(r.x, y0, r.x + r.length, y0)
   346             }
   347           }
   348         }
   349       }
   350     }
   351   }
   352 
   353 
   354   /* text */
   355 
   356   private def caret_enabled: Boolean =
   357     caret_visible && (!text_area.hasFocus || text_area.isCaretVisible)
   358 
   359   private def caret_color(rendering: Rendering, offset: Text.Offset): Color =
   360   {
   361     if (text_area.isCaretVisible) text_area.getPainter.getCaretColor
   362     else {
   363       val debug_positions =
   364         (for {
   365           c <- Debugger.focus().iterator
   366           pos <- c.debug_position.iterator
   367         } yield pos).toList
   368       if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _)))
   369         rendering.caret_debugger_color
   370       else rendering.caret_invisible_color
   371     }
   372   }
   373 
   374   private def paint_chunk_list(rendering: Rendering,
   375     gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   376   {
   377     val clip_rect = gfx.getClipBounds
   378     val painter = text_area.getPainter
   379     val font_context = painter.getFontRenderContext
   380 
   381     val caret_range =
   382       if (caret_enabled) JEdit_Lib.caret_range(text_area)
   383       else Text.Range.offside
   384 
   385     var w = 0.0f
   386     var chunk = head
   387     while (chunk != null) {
   388       val chunk_offset = line_start + chunk.offset
   389       if (x + w + chunk.width > clip_rect.x &&
   390           x + w < clip_rect.x + clip_rect.width && chunk.length > 0)
   391       {
   392         val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
   393         val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
   394         val chunk_font = chunk.style.getFont
   395         val chunk_color = chunk.style.getForegroundColor
   396 
   397         def string_width(s: String): Float =
   398           if (s.isEmpty) 0.0f
   399           else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
   400 
   401         val markup =
   402           for {
   403             r1 <- rendering.text_color(chunk_range, chunk_color)
   404             r2 <- r1.try_restrict(chunk_range)
   405           } yield r2
   406 
   407         val padded_markup_iterator =
   408           if (markup.isEmpty)
   409             Iterator(Text.Info(chunk_range, chunk_color))
   410           else
   411             Iterator(
   412               Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
   413             markup.iterator ++
   414             Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
   415 
   416         var x1 = x + w
   417         gfx.setFont(chunk_font)
   418         for (Text.Info(range, color) <- padded_markup_iterator if !range.is_singularity) {
   419           val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
   420           gfx.setColor(color)
   421 
   422           range.try_restrict(caret_range) match {
   423             case Some(r) if !r.is_singularity =>
   424               val i = r.start - range.start
   425               val j = r.stop - range.start
   426               val s1 = str.substring(0, i)
   427               val s2 = str.substring(i, j)
   428               val s3 = str.substring(j)
   429 
   430               if (s1.nonEmpty) gfx.drawString(Word.bidi_override(s1), x1, y)
   431 
   432               val astr = new AttributedString(Word.bidi_override(s2))
   433               astr.addAttribute(TextAttribute.FONT, chunk_font)
   434               astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, r.start))
   435               astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
   436               gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
   437 
   438               if (s3.nonEmpty)
   439                 gfx.drawString(Word.bidi_override(s3), x1 + string_width(str.substring(0, j)), y)
   440 
   441             case _ =>
   442               gfx.drawString(Word.bidi_override(str), x1, y)
   443           }
   444           x1 += string_width(str)
   445         }
   446       }
   447       w += chunk.width
   448       chunk = chunk.next.asInstanceOf[Chunk]
   449     }
   450     w
   451   }
   452 
   453   private val text_painter = new TextAreaExtension
   454   {
   455     override def paintScreenLineRange(gfx: Graphics2D,
   456       first_line: Int, last_line: Int, physical_lines: Array[Int],
   457       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   458     {
   459       robust_rendering { rendering =>
   460         val painter = text_area.getPainter
   461         val fm = painter.getFontMetrics
   462         val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext)
   463 
   464         val clip = gfx.getClip
   465         val x0 = text_area.getHorizontalOffset
   466         var y0 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent
   467 
   468         val (bullet_x, bullet_y, bullet_w, bullet_h) =
   469         {
   470           val w = fm.charWidth(' ')
   471           val b = (w / 2) max 1
   472           val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt
   473           ((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
   474         }
   475 
   476         for (i <- 0 until physical_lines.length) {
   477           val line = physical_lines(i)
   478           if (line != -1) {
   479             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
   480 
   481             // text chunks
   482             val screen_line = first_line + i
   483             val chunks = text_area.getChunksOfScreenLine(screen_line)
   484             if (chunks != null) {
   485               try {
   486                 val line_start = buffer.getLineStartOffset(line)
   487                 gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
   488                 val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
   489                 gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   490                 orig_text_painter.paintValidLine(gfx,
   491                   screen_line, line, start(i), end(i), y + line_height * i)
   492               } finally { gfx.setClip(clip) }
   493             }
   494 
   495             // bullet bar
   496             for {
   497               Text.Info(range, color) <- rendering.bullet(line_range)
   498               r <- JEdit_Lib.gfx_range(text_area, range)
   499             } {
   500               gfx.setColor(color)
   501               gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y,
   502                 r.length - bullet_w, line_height - bullet_h)
   503             }
   504           }
   505           y0 += line_height
   506         }
   507       }
   508     }
   509   }
   510 
   511 
   512   /* foreground */
   513 
   514   private val foreground_painter = new TextAreaExtension
   515   {
   516     override def paintScreenLineRange(gfx: Graphics2D,
   517       first_line: Int, last_line: Int, physical_lines: Array[Int],
   518       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   519     {
   520       robust_rendering { rendering =>
   521         val search_pattern = get_search_pattern()
   522         for (i <- 0 until physical_lines.length) {
   523           if (physical_lines(i) != -1) {
   524             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
   525 
   526             // foreground color
   527             for {
   528               Text.Info(range, color) <- rendering.foreground(line_range)
   529               r <- JEdit_Lib.gfx_range(text_area, range)
   530             } {
   531               gfx.setColor(color)
   532               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   533             }
   534 
   535             // search pattern
   536             for {
   537               regex <- search_pattern
   538               text <- JEdit_Lib.try_get_text(buffer, line_range)
   539               m <- regex.findAllMatchIn(text)
   540               range = Text.Range(m.start, m.end) + line_range.start
   541               r <- JEdit_Lib.gfx_range(text_area, range)
   542             } {
   543               gfx.setColor(rendering.search_color)
   544               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   545             }
   546 
   547             // highlight range -- potentially from other snapshot
   548             for {
   549               info <- highlight_area.info
   550               Text.Info(range, color) <- info.try_restrict(line_range)
   551               r <- JEdit_Lib.gfx_range(text_area, range)
   552             } {
   553               gfx.setColor(color)
   554               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   555             }
   556 
   557             // hyperlink range -- potentially from other snapshot
   558             for {
   559               info <- hyperlink_area.info
   560               Text.Info(range, _) <- info.try_restrict(line_range)
   561               r <- JEdit_Lib.gfx_range(text_area, range)
   562             } {
   563               gfx.setColor(rendering.hyperlink_color)
   564               gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
   565             }
   566 
   567             // completion range
   568             if (!hyperlink_area.is_active && caret_visible) {
   569               for {
   570                 completion <- Completion_Popup.Text_Area(text_area)
   571                 Text.Info(range, color) <- completion.rendering(rendering, line_range)
   572                 r <- JEdit_Lib.gfx_range(text_area, range)
   573               } {
   574                 gfx.setColor(color)
   575                 gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
   576               }
   577             }
   578           }
   579         }
   580       }
   581     }
   582   }
   583 
   584 
   585   /* caret -- outside of text range */
   586 
   587   private class Caret_Painter(before: Boolean) extends TextAreaExtension
   588   {
   589     override def paintValidLine(gfx: Graphics2D,
   590       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   591     {
   592       robust_rendering { _ =>
   593         if (before) gfx.clipRect(0, 0, 0, 0)
   594         else gfx.setClip(painter_clip)
   595       }
   596     }
   597   }
   598 
   599   private val before_caret_painter1 = new Caret_Painter(true)
   600   private val after_caret_painter1 = new Caret_Painter(false)
   601   private val before_caret_painter2 = new Caret_Painter(true)
   602   private val after_caret_painter2 = new Caret_Painter(false)
   603 
   604   private val caret_painter = new TextAreaExtension
   605   {
   606     override def paintValidLine(gfx: Graphics2D,
   607       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   608     {
   609       robust_rendering { rendering =>
   610         if (caret_visible) {
   611           val caret = text_area.getCaretPosition
   612           if (caret_enabled && start <= caret && caret == end - 1) {
   613             val painter = text_area.getPainter
   614             val fm = painter.getFontMetrics
   615 
   616             val offset = caret - text_area.getLineStartOffset(physical_line)
   617             val x = text_area.offsetToXY(physical_line, offset).x
   618             val y1 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent
   619 
   620             val astr = new AttributedString(" ")
   621             astr.addAttribute(TextAttribute.FONT, painter.getFont)
   622             astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, caret))
   623             astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
   624 
   625             val clip = gfx.getClip
   626             try {
   627               gfx.clipRect(x, y, Integer.MAX_VALUE, painter.getLineHeight)
   628               gfx.drawString(astr.getIterator, x, y1)
   629             }
   630             finally { gfx.setClip(clip) }
   631           }
   632         }
   633       }
   634     }
   635   }
   636 
   637 
   638   /* activation */
   639 
   640   def activate()
   641   {
   642     val painter = text_area.getPainter
   643     painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
   644     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   645     painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
   646     painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
   647     painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
   648     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
   649     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
   650     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
   651     painter.addExtension(500, foreground_painter)
   652     painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
   653     painter.removeExtension(orig_text_painter)
   654     painter.addMouseListener(mouse_listener)
   655     painter.addMouseMotionListener(mouse_motion_listener)
   656     text_area.addFocusListener(focus_listener)
   657     view.addWindowListener(window_listener)
   658   }
   659 
   660   def deactivate()
   661   {
   662     active_reset()
   663     val painter = text_area.getPainter
   664     view.removeWindowListener(window_listener)
   665     text_area.removeFocusListener(focus_listener)
   666     painter.removeMouseMotionListener(mouse_motion_listener)
   667     painter.removeMouseListener(mouse_listener)
   668     painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   669     painter.removeExtension(reset_state)
   670     painter.removeExtension(foreground_painter)
   671     painter.removeExtension(caret_painter)
   672     painter.removeExtension(after_caret_painter2)
   673     painter.removeExtension(before_caret_painter2)
   674     painter.removeExtension(after_caret_painter1)
   675     painter.removeExtension(before_caret_painter1)
   676     painter.removeExtension(text_painter)
   677     painter.removeExtension(background_painter)
   678     painter.removeExtension(set_state)
   679   }
   680 }