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