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