src/Tools/jEdit/src/text_area_painter.scala
author wenzelm
Wed Jun 15 16:26:09 2011 +0200 (2011-06-15)
changeset 43398 c3e2a361b418
parent 43396 548a68eafaea
child 43404 c8369f3d88a1
permissions -rw-r--r--
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
     1 /*  Title:      Tools/jEdit/src/text_area_painter.scala
     2     Author:     Makarius
     3 
     4 Painter setup for main jEdit text area.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.{Graphics2D, Shape}
    13 import java.awt.font.TextAttribute
    14 import java.text.AttributedString
    15 import java.util.ArrayList
    16 
    17 import org.gjt.sp.util.Log
    18 
    19 import org.gjt.sp.jedit.Debug
    20 import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
    21 import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, JEditTextArea}
    22 
    23 
    24 class Text_Area_Painter(doc_view: Document_View)
    25 {
    26   private val model = doc_view.model
    27   private val buffer = model.buffer
    28   private val text_area = doc_view.text_area
    29 
    30   private def painter_body(body: => Unit)
    31   {
    32     if (buffer == text_area.getBuffer)
    33       Swing_Thread.now {
    34         try { Isabelle.buffer_lock(buffer) { body } }
    35         catch { case t: Throwable => Log.log(Log.ERROR, this, t) }
    36       }
    37   }
    38 
    39 
    40   /* original painters */
    41 
    42   private def pick_extension(name: String): TextAreaExtension =
    43   {
    44     text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
    45     match {
    46       case List(x) => x
    47       case _ => error("Expected exactly one " + name)
    48     }
    49   }
    50 
    51   private val orig_text_painter =
    52     pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
    53 
    54 
    55   /* common painter state */
    56 
    57   @volatile private var painter_snapshot: Document.Snapshot = null
    58   @volatile private var painter_clip: Shape = null
    59 
    60   private val set_state = new TextAreaExtension
    61   {
    62     override def paintScreenLineRange(gfx: Graphics2D,
    63       first_line: Int, last_line: Int, physical_lines: Array[Int],
    64       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    65     {
    66       painter_snapshot = model.snapshot()
    67       painter_clip = gfx.getClip
    68     }
    69   }
    70 
    71   private val reset_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_snapshot = null
    78       painter_clip = null
    79     }
    80   }
    81 
    82 
    83   /* text background */
    84 
    85   private val background_painter = new TextAreaExtension
    86   {
    87     override def paintScreenLineRange(gfx: Graphics2D,
    88       first_line: Int, last_line: Int, physical_lines: Array[Int],
    89       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    90     {
    91       painter_body {
    92         val snapshot = painter_snapshot
    93         val ascent = text_area.getPainter.getFontMetrics.getAscent
    94 
    95         for (i <- 0 until physical_lines.length) {
    96           if (physical_lines(i) != -1) {
    97             val line_range = doc_view.proper_line_range(start(i), end(i))
    98 
    99             // background color: status
   100             val cmds = snapshot.node.command_range(snapshot.revert(line_range))
   101             for {
   102               (command, command_start) <- cmds if !command.is_ignored
   103               val range = line_range.restrict(snapshot.convert(command.range + command_start))
   104               r <- Isabelle.gfx_range(text_area, range)
   105               color <- Isabelle_Markup.status_color(snapshot, command)
   106             } {
   107               gfx.setColor(color)
   108               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   109             }
   110 
   111             // background color (1): markup
   112             for {
   113               Text.Info(range, Some(color)) <-
   114                 snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
   115               r <- Isabelle.gfx_range(text_area, range)
   116             } {
   117               gfx.setColor(color)
   118               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   119             }
   120 
   121             // background color (2): markup
   122             for {
   123               Text.Info(range, Some(color)) <-
   124                 snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
   125               r <- Isabelle.gfx_range(text_area, range)
   126             } {
   127               gfx.setColor(color)
   128               gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
   129             }
   130 
   131             // sub-expression highlighting -- potentially from other snapshot
   132             doc_view.highlight_range match {
   133               case Some((range, color)) if line_range.overlaps(range) =>
   134                 Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
   135                   case None =>
   136                   case Some(r) =>
   137                     gfx.setColor(color)
   138                     gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
   139                 }
   140               case _ =>
   141             }
   142 
   143             // squiggly underline
   144             for {
   145               Text.Info(range, Some(color)) <-
   146                 snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
   147               r <- Isabelle.gfx_range(text_area, range)
   148             } {
   149               gfx.setColor(color)
   150               val x0 = (r.x / 2) * 2
   151               val y0 = r.y + ascent + 1
   152               for (x1 <- Range(x0, x0 + r.length, 2)) {
   153                 val y1 = if (x1 % 4 < 2) y0 else y0 + 1
   154                 gfx.drawLine(x1, y1, x1 + 1, y1)
   155               }
   156             }
   157           }
   158         }
   159       }
   160     }
   161   }
   162 
   163 
   164   /* text */
   165 
   166   def char_width(): Int =
   167   {
   168     val painter = text_area.getPainter
   169     val font = painter.getFont
   170     val font_context = painter.getFontRenderContext
   171     font.getStringBounds(" ", font_context).getWidth.round.toInt
   172   }
   173 
   174   private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
   175   {
   176     val painter = text_area.getPainter
   177     val font = painter.getFont
   178     val font_context = painter.getFontRenderContext
   179 
   180     // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
   181     // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
   182     val margin =
   183       if (buffer.getStringProperty("wrap") != "soft") 0.0f
   184       else {
   185         val max = buffer.getIntegerProperty("maxLineLen", 0)
   186         if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
   187         else painter.getWidth - char_width() * 3
   188       }.toFloat
   189 
   190     val out = new ArrayList[Chunk]
   191     val handler = new DisplayTokenHandler
   192 
   193     var result = Map[Text.Offset, Chunk]()
   194     for (line <- physical_lines) {
   195       out.clear
   196       handler.init(painter.getStyles, font_context, painter, out, margin)
   197       buffer.markTokens(line, handler)
   198 
   199       val line_start = buffer.getLineStartOffset(line)
   200       for (i <- 0 until out.size) {
   201         val chunk = out.get(i)
   202         result += (line_start + chunk.offset -> chunk)
   203       }
   204     }
   205     result
   206   }
   207 
   208   private def paint_chunk_list(gfx: Graphics2D,
   209     offset: Text.Offset, caret_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   210   {
   211     val clip_rect = gfx.getClipBounds
   212     val painter = text_area.getPainter
   213     val font_context = painter.getFontRenderContext
   214 
   215     var w = 0.0f
   216     var chunk_offset = offset
   217     var chunk = head
   218     while (chunk != null) {
   219       val chunk_length = if (chunk.str == null) 0 else chunk.str.length
   220 
   221       if (x + w + chunk.width > clip_rect.x &&
   222           x + w < clip_rect.x + clip_rect.width &&
   223           chunk.accessable && chunk.visible)
   224       {
   225         val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk_length)
   226         val chunk_font = chunk.style.getFont
   227         val chunk_color = chunk.style.getForegroundColor
   228 
   229         val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
   230 
   231         gfx.setFont(chunk_font)
   232         if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
   233             markup.forall(info => info.info.isEmpty) &&
   234             !chunk_range.contains(caret_offset)) {
   235           gfx.setColor(chunk_color)
   236           gfx.drawGlyphVector(chunk.gv, x + w, y)
   237         }
   238         else {
   239           var x1 = x + w
   240           for (Text.Info(range, info) <- markup) {
   241             val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
   242             gfx.setColor(info.getOrElse(chunk_color))
   243             if (range.contains(caret_offset)) {
   244               val astr = new AttributedString(str)
   245               val i = caret_offset - range.start
   246               astr.addAttribute(TextAttribute.FONT, chunk_font)
   247               astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, i + 1)
   248               astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, i + 1)
   249               gfx.drawString(astr.getIterator, x1.toInt, y.toInt)
   250             }
   251             else {
   252               gfx.drawString(str, x1.toInt, y.toInt)
   253             }
   254             x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
   255           }
   256         }
   257       }
   258       w += chunk.width
   259       chunk_offset += chunk_length
   260       chunk = chunk.next.asInstanceOf[Chunk]
   261     }
   262     w
   263   }
   264 
   265   private val text_painter = new TextAreaExtension
   266   {
   267     override def paintScreenLineRange(gfx: Graphics2D,
   268       first_line: Int, last_line: Int, physical_lines: Array[Int],
   269       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   270     {
   271       painter_body {
   272         val clip = gfx.getClip
   273         val x0 = text_area.getHorizontalOffset
   274         val fm = text_area.getPainter.getFontMetrics
   275         var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
   276 
   277         val caret_offset =
   278           if (text_area.hasFocus) text_area.getCaretPosition
   279           else -1
   280 
   281         val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
   282         for (i <- 0 until physical_lines.length) {
   283           if (physical_lines(i) != -1) {
   284             val x1 =
   285               infos.get(start(i)) match {
   286                 case None => x0
   287                 case Some(chunk) =>
   288                   gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
   289                   val w = paint_chunk_list(gfx, start(i), caret_offset, chunk, x0, y0).toInt
   290                   x0 + w.toInt
   291               }
   292             gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   293             orig_text_painter.paintValidLine(gfx,
   294               first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
   295             gfx.setClip(clip)
   296           }
   297           y0 += line_height
   298         }
   299       }
   300     }
   301   }
   302 
   303 
   304   /* caret -- outside of text range */
   305 
   306   private class Caret_Painter(before: Boolean) extends TextAreaExtension
   307   {
   308     override def paintValidLine(gfx: Graphics2D,
   309       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   310     {
   311       if (before) gfx.clipRect(0, 0, 0, 0)
   312       else gfx.setClip(painter_clip)
   313     }
   314   }
   315 
   316   private val before_caret_painter1 = new Caret_Painter(true)
   317   private val after_caret_painter1 = new Caret_Painter(false)
   318   private val before_caret_painter2 = new Caret_Painter(true)
   319   private val after_caret_painter2 = new Caret_Painter(false)
   320 
   321   private val caret_painter = new TextAreaExtension
   322   {
   323     override def paintValidLine(gfx: Graphics2D,
   324       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   325     {
   326       painter_body {
   327         if (text_area.hasFocus) {
   328           val caret = text_area.getCaretPosition
   329           if (start <= caret && caret == end - 1) {
   330             val painter = text_area.getPainter
   331             val fm = painter.getFontMetrics
   332 
   333             val offset = caret - text_area.getLineStartOffset(physical_line)
   334             val x = text_area.offsetToXY(physical_line, offset).x
   335             gfx.setColor(painter.getCaretColor)
   336             gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1)
   337           }
   338         }
   339       }
   340     }
   341   }
   342 
   343 
   344   /* activation */
   345 
   346   def activate()
   347   {
   348     val painter = text_area.getPainter
   349     painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
   350     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   351     painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
   352     painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
   353     painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
   354     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
   355     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
   356     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
   357     painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
   358     painter.removeExtension(orig_text_painter)
   359   }
   360 
   361   def deactivate()
   362   {
   363     val painter = text_area.getPainter
   364     painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   365     painter.removeExtension(reset_state)
   366     painter.removeExtension(caret_painter)
   367     painter.removeExtension(after_caret_painter2)
   368     painter.removeExtension(before_caret_painter2)
   369     painter.removeExtension(after_caret_painter1)
   370     painter.removeExtension(before_caret_painter1)
   371     painter.removeExtension(text_painter)
   372     painter.removeExtension(background_painter)
   373     painter.removeExtension(set_state)
   374   }
   375 }
   376