src/Tools/jEdit/src/text_area_painter.scala
author wenzelm
Wed Mar 14 15:37:51 2012 +0100 (2012-03-14)
changeset 46920 5f44c8bea84e
parent 46913 3444a24dc4e9
child 47027 fc3bb6c02a3c
permissions -rw-r--r--
more explicit indication of swing thread context;
     1 /*  Title:      Tools/jEdit/src/text_area_painter.scala
     2     Author:     Makarius
     3 
     4 Painter setup for main jEdit text area, depending on common snapshot.
     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.jedit.Debug
    18 import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
    19 import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
    20 
    21 
    22 class Text_Area_Painter(doc_view: Document_View)
    23 {
    24   private val model = doc_view.model
    25   private val buffer = model.buffer
    26   private val text_area = doc_view.text_area
    27 
    28 
    29   /* graphics range */
    30 
    31   private def char_width(): Int =
    32   {
    33     val painter = text_area.getPainter
    34     val font = painter.getFont
    35     val font_context = painter.getFontRenderContext
    36     font.getStringBounds(" ", font_context).getWidth.round.toInt
    37   }
    38 
    39   private class Gfx_Range(val x: Int, val y: Int, val length: Int)
    40 
    41   // NB: jEdit already normalizes \r\n and \r to \n
    42   // NB: last line lacks \n
    43   private def gfx_range(range: Text.Range): Option[Gfx_Range] =
    44   {
    45     val p = text_area.offsetToXY(range.start)
    46 
    47     val end = buffer.getLength
    48     val stop = range.stop
    49     val (q, r) =
    50       if (stop >= end) (text_area.offsetToXY(end), char_width())
    51       else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
    52         (text_area.offsetToXY(stop - 1), char_width())
    53       else (text_area.offsetToXY(stop), 0)
    54 
    55     if (p != null && q != null && p.x < q.x + r && p.y == q.y)
    56       Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
    57     else None
    58   }
    59 
    60 
    61   /* original painters */
    62 
    63   private def pick_extension(name: String): TextAreaExtension =
    64   {
    65     text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
    66     match {
    67       case List(x) => x
    68       case _ => error("Expected exactly one " + name)
    69     }
    70   }
    71 
    72   private val orig_text_painter =
    73     pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
    74 
    75 
    76   /* common painter state */
    77 
    78   @volatile private var painter_snapshot: Document.Snapshot = null
    79   @volatile private var painter_clip: Shape = null
    80 
    81   private val set_state = new TextAreaExtension
    82   {
    83     override def paintScreenLineRange(gfx: Graphics2D,
    84       first_line: Int, last_line: Int, physical_lines: Array[Int],
    85       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    86     {
    87       painter_snapshot = doc_view.update_snapshot()
    88       painter_clip = gfx.getClip
    89     }
    90   }
    91 
    92   private val reset_state = new TextAreaExtension
    93   {
    94     override def paintScreenLineRange(gfx: Graphics2D,
    95       first_line: Int, last_line: Int, physical_lines: Array[Int],
    96       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    97     {
    98       painter_snapshot = null
    99       painter_clip = null
   100     }
   101   }
   102 
   103   private def robust_snapshot(body: Document.Snapshot => Unit)
   104   {
   105     doc_view.robust_body(()) { body(painter_snapshot) }
   106   }
   107 
   108 
   109   /* text background */
   110 
   111   private val background_painter = new TextAreaExtension
   112   {
   113     override def paintScreenLineRange(gfx: Graphics2D,
   114       first_line: Int, last_line: Int, physical_lines: Array[Int],
   115       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   116     {
   117       robust_snapshot { snapshot =>
   118         val ascent = text_area.getPainter.getFontMetrics.getAscent
   119 
   120         for (i <- 0 until physical_lines.length) {
   121           if (physical_lines(i) != -1) {
   122             val line_range = doc_view.proper_line_range(start(i), end(i))
   123 
   124             // background color (1)
   125             for {
   126               Text.Info(range, color) <- Isabelle_Rendering.background1(snapshot, line_range)
   127               r <- gfx_range(range)
   128             } {
   129               gfx.setColor(color)
   130               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   131             }
   132 
   133             // background color (2)
   134             for {
   135               Text.Info(range, color) <- Isabelle_Rendering.background2(snapshot, line_range)
   136               r <- gfx_range(range)
   137             } {
   138               gfx.setColor(color)
   139               gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
   140             }
   141 
   142             // squiggly underline
   143             for {
   144               Text.Info(range, color) <- Isabelle_Rendering.squiggly_underline(snapshot, line_range)
   145               r <- gfx_range(range)
   146             } {
   147               gfx.setColor(color)
   148               val x0 = (r.x / 2) * 2
   149               val y0 = r.y + ascent + 1
   150               for (x1 <- Range(x0, x0 + r.length, 2)) {
   151                 val y1 = if (x1 % 4 < 2) y0 else y0 + 1
   152                 gfx.drawLine(x1, y1, x1 + 1, y1)
   153               }
   154             }
   155           }
   156         }
   157       }
   158     }
   159   }
   160 
   161 
   162   /* text */
   163 
   164   private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
   165   {
   166     val painter = text_area.getPainter
   167     val font = painter.getFont
   168     val font_context = painter.getFontRenderContext
   169 
   170     // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
   171     // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
   172     val margin =
   173       if (buffer.getStringProperty("wrap") != "soft") 0.0f
   174       else {
   175         val max = buffer.getIntegerProperty("maxLineLen", 0)
   176         if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
   177         else painter.getWidth - char_width() * 3
   178       }.toFloat
   179 
   180     val out = new ArrayList[Chunk]
   181     val handler = new DisplayTokenHandler
   182 
   183     var result = Map[Text.Offset, Chunk]()
   184     for (line <- physical_lines) {
   185       val line_start = buffer.getLineStartOffset(line)
   186 
   187       out.clear
   188       handler.init(painter.getStyles, font_context, painter, out, margin, line_start)
   189       buffer.markTokens(line, handler)
   190 
   191       for (i <- 0 until out.size) {
   192         val chunk = out.get(i)
   193         result += (line_start + chunk.offset -> chunk)
   194       }
   195     }
   196     result
   197   }
   198 
   199   private def paint_chunk_list(snapshot: Document.Snapshot,
   200     gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   201   {
   202     val clip_rect = gfx.getClipBounds
   203     val painter = text_area.getPainter
   204     val font_context = painter.getFontRenderContext
   205 
   206     var w = 0.0f
   207     var chunk = head
   208     while (chunk != null) {
   209       val chunk_offset = line_start + chunk.offset
   210       if (x + w + chunk.width > clip_rect.x &&
   211           x + w < clip_rect.x + clip_rect.width && chunk.accessable)
   212       {
   213         val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
   214         val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
   215         val chunk_font = chunk.style.getFont
   216         val chunk_color = chunk.style.getForegroundColor
   217 
   218         def string_width(s: String): Float =
   219           if (s.isEmpty) 0.0f
   220           else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
   221 
   222         val caret_range =
   223           if (text_area.hasFocus) doc_view.caret_range()
   224           else Text.Range(-1)
   225 
   226         val markup =
   227           for {
   228             r1 <- Isabelle_Rendering.text_color(snapshot, chunk_range, chunk_color)
   229             r2 <- r1.try_restrict(chunk_range)
   230           } yield r2
   231 
   232         val padded_markup =
   233           if (markup.isEmpty)
   234             Iterator(Text.Info(chunk_range, chunk_color))
   235           else
   236             Iterator(
   237               Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
   238             markup.iterator ++
   239             Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
   240 
   241         var x1 = x + w
   242         gfx.setFont(chunk_font)
   243         for (Text.Info(range, color) <- padded_markup if !range.is_singularity) {
   244           val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
   245           gfx.setColor(color)
   246 
   247           range.try_restrict(caret_range) match {
   248             case Some(r) if !r.is_singularity =>
   249               val i = r.start - range.start
   250               val j = r.stop - range.start
   251               val s1 = str.substring(0, i)
   252               val s2 = str.substring(i, j)
   253               val s3 = str.substring(j)
   254 
   255               if (!s1.isEmpty) gfx.drawString(s1, x1, y)
   256 
   257               val astr = new AttributedString(s2)
   258               astr.addAttribute(TextAttribute.FONT, chunk_font)
   259               astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
   260               astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
   261               gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
   262 
   263               if (!s3.isEmpty)
   264                 gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
   265 
   266             case _ =>
   267               gfx.drawString(str, x1, y)
   268           }
   269           x1 += string_width(str)
   270         }
   271       }
   272       w += chunk.width
   273       chunk = chunk.next.asInstanceOf[Chunk]
   274     }
   275     w
   276   }
   277 
   278   private val text_painter = new TextAreaExtension
   279   {
   280     override def paintScreenLineRange(gfx: Graphics2D,
   281       first_line: Int, last_line: Int, physical_lines: Array[Int],
   282       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   283     {
   284       robust_snapshot { snapshot =>
   285         val clip = gfx.getClip
   286         val x0 = text_area.getHorizontalOffset
   287         val fm = text_area.getPainter.getFontMetrics
   288         var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
   289 
   290         val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
   291         for (i <- 0 until physical_lines.length) {
   292           if (physical_lines(i) != -1) {
   293             val x1 =
   294               infos.get(start(i)) match {
   295                 case None => x0
   296                 case Some(chunk) =>
   297                   gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
   298                   val w = paint_chunk_list(snapshot, gfx, start(i), chunk, x0, y0).toInt
   299                   x0 + w.toInt
   300               }
   301             gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   302             orig_text_painter.paintValidLine(gfx,
   303               first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
   304             gfx.setClip(clip)
   305           }
   306           y0 += line_height
   307         }
   308       }
   309     }
   310   }
   311 
   312 
   313   /* foreground */
   314 
   315   private val foreground_painter = new TextAreaExtension
   316   {
   317     override def paintScreenLineRange(gfx: Graphics2D,
   318       first_line: Int, last_line: Int, physical_lines: Array[Int],
   319       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   320     {
   321       robust_snapshot { snapshot =>
   322         for (i <- 0 until physical_lines.length) {
   323           if (physical_lines(i) != -1) {
   324             val line_range = doc_view.proper_line_range(start(i), end(i))
   325 
   326             // foreground color
   327             for {
   328               Text.Info(range, color) <- Isabelle_Rendering.foreground(snapshot, line_range)
   329               r <- gfx_range(range)
   330             } {
   331               gfx.setColor(color)
   332               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   333             }
   334 
   335             // highlighted range -- potentially from other snapshot
   336             for {
   337               info <- doc_view.highlight_range()
   338               Text.Info(range, color) <- info.try_restrict(line_range)
   339               r <- gfx_range(range)
   340             } {
   341               gfx.setColor(color)
   342               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   343             }
   344           }
   345         }
   346       }
   347     }
   348   }
   349 
   350 
   351   /* caret -- outside of text range */
   352 
   353   private class Caret_Painter(before: Boolean) extends TextAreaExtension
   354   {
   355     override def paintValidLine(gfx: Graphics2D,
   356       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   357     {
   358       robust_snapshot { _ =>
   359         if (before) gfx.clipRect(0, 0, 0, 0)
   360         else gfx.setClip(painter_clip)
   361       }
   362     }
   363   }
   364 
   365   private val before_caret_painter1 = new Caret_Painter(true)
   366   private val after_caret_painter1 = new Caret_Painter(false)
   367   private val before_caret_painter2 = new Caret_Painter(true)
   368   private val after_caret_painter2 = new Caret_Painter(false)
   369 
   370   private val caret_painter = new TextAreaExtension
   371   {
   372     override def paintValidLine(gfx: Graphics2D,
   373       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   374     {
   375       robust_snapshot { _ =>
   376         if (text_area.hasFocus) {
   377           val caret = text_area.getCaretPosition
   378           if (start <= caret && caret == end - 1) {
   379             val painter = text_area.getPainter
   380             val fm = painter.getFontMetrics
   381 
   382             val offset = caret - text_area.getLineStartOffset(physical_line)
   383             val x = text_area.offsetToXY(physical_line, offset).x
   384             gfx.setColor(painter.getCaretColor)
   385             gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1)
   386           }
   387         }
   388       }
   389     }
   390   }
   391 
   392 
   393   /* activation */
   394 
   395   def activate()
   396   {
   397     val painter = text_area.getPainter
   398     painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
   399     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   400     painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
   401     painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
   402     painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
   403     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
   404     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
   405     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
   406     painter.addExtension(500, foreground_painter)
   407     painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
   408     painter.removeExtension(orig_text_painter)
   409   }
   410 
   411   def deactivate()
   412   {
   413     val painter = text_area.getPainter
   414     painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   415     painter.removeExtension(reset_state)
   416     painter.removeExtension(foreground_painter)
   417     painter.removeExtension(caret_painter)
   418     painter.removeExtension(after_caret_painter2)
   419     painter.removeExtension(before_caret_painter2)
   420     painter.removeExtension(after_caret_painter1)
   421     painter.removeExtension(before_caret_painter1)
   422     painter.removeExtension(text_painter)
   423     painter.removeExtension(background_painter)
   424     painter.removeExtension(set_state)
   425   }
   426 }
   427