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