src/Tools/jEdit/src/text_area_painter.scala
author wenzelm
Wed Jun 15 11:41:49 2011 +0200 (2011-06-15)
changeset 43392 fe4b8c52b1cc
parent 43383 63fc6b5ef8ac
child 43393 f4141da52e92
permissions -rw-r--r--
paint caret according to precise font metrics;
     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
    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, JEditTextArea}
    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   /* original painters */
    30 
    31   private def pick_extension(name: String): TextAreaExtension =
    32   {
    33     text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
    34     match {
    35       case List(x) => x
    36       case _ => error("Expected exactly one " + name)
    37     }
    38   }
    39 
    40   private val orig_text_painter =
    41     pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
    42 
    43   private val orig_caret_painter =
    44     pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintCaret")
    45 
    46 
    47   /* painter snapshot */
    48 
    49   @volatile private var _painter_snapshot: Option[Document.Snapshot] = None
    50 
    51   private def painter_snapshot(): Document.Snapshot =
    52     _painter_snapshot match {
    53       case Some(snapshot) => snapshot
    54       case None => error("Missing document snapshot for text area painter")
    55     }
    56 
    57   private val set_snapshot = new TextAreaExtension
    58   {
    59     override def paintScreenLineRange(gfx: Graphics2D,
    60       first_line: Int, last_line: Int, physical_lines: Array[Int],
    61       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    62     {
    63       _painter_snapshot = Some(model.snapshot())
    64     }
    65   }
    66 
    67   private val reset_snapshot = new TextAreaExtension
    68   {
    69     override def paintScreenLineRange(gfx: Graphics2D,
    70       first_line: Int, last_line: Int, physical_lines: Array[Int],
    71       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    72     {
    73       _painter_snapshot = None
    74     }
    75   }
    76 
    77 
    78   /* text background */
    79 
    80   private val background_painter = new TextAreaExtension
    81   {
    82     override def paintScreenLineRange(gfx: Graphics2D,
    83       first_line: Int, last_line: Int, physical_lines: Array[Int],
    84       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    85     {
    86       Isabelle.swing_buffer_lock(buffer) {
    87         val snapshot = painter_snapshot()
    88         val ascent = text_area.getPainter.getFontMetrics.getAscent
    89 
    90         for (i <- 0 until physical_lines.length) {
    91           if (physical_lines(i) != -1) {
    92             val line_range = doc_view.proper_line_range(start(i), end(i))
    93 
    94             // background color: status
    95             val cmds = snapshot.node.command_range(snapshot.revert(line_range))
    96             for {
    97               (command, command_start) <- cmds if !command.is_ignored
    98               val range = line_range.restrict(snapshot.convert(command.range + command_start))
    99               r <- Isabelle.gfx_range(text_area, range)
   100               color <- Isabelle_Markup.status_color(snapshot, command)
   101             } {
   102               gfx.setColor(color)
   103               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   104             }
   105 
   106             // background color (1): markup
   107             for {
   108               Text.Info(range, Some(color)) <-
   109                 snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
   110               r <- Isabelle.gfx_range(text_area, range)
   111             } {
   112               gfx.setColor(color)
   113               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   114             }
   115 
   116             // background color (2): markup
   117             for {
   118               Text.Info(range, Some(color)) <-
   119                 snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
   120               r <- Isabelle.gfx_range(text_area, range)
   121             } {
   122               gfx.setColor(color)
   123               gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
   124             }
   125 
   126             // sub-expression highlighting -- potentially from other snapshot
   127             doc_view.highlight_range match {
   128               case Some((range, color)) if line_range.overlaps(range) =>
   129                 Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
   130                   case None =>
   131                   case Some(r) =>
   132                     gfx.setColor(color)
   133                     gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
   134                 }
   135               case _ =>
   136             }
   137 
   138             // squiggly underline
   139             for {
   140               Text.Info(range, Some(color)) <-
   141                 snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
   142               r <- Isabelle.gfx_range(text_area, range)
   143             } {
   144               gfx.setColor(color)
   145               val x0 = (r.x / 2) * 2
   146               val y0 = r.y + ascent + 1
   147               for (x1 <- Range(x0, x0 + r.length, 2)) {
   148                 val y1 = if (x1 % 4 < 2) y0 else y0 + 1
   149                 gfx.drawLine(x1, y1, x1 + 1, y1)
   150               }
   151             }
   152           }
   153         }
   154       }
   155     }
   156   }
   157 
   158 
   159   /* text */
   160 
   161   private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
   162   {
   163     val painter = text_area.getPainter
   164     val font = painter.getFont
   165     val font_context = painter.getFontRenderContext
   166 
   167     // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
   168     // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
   169     val margin =
   170       if (buffer.getStringProperty("wrap") != "soft") 0.0f
   171       else {
   172         val max = buffer.getIntegerProperty("maxLineLen", 0)
   173         if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
   174         else painter.getWidth - font.getStringBounds(" ", font_context).getWidth.round.toInt * 3
   175       }.toFloat
   176 
   177     val out = new ArrayList[Chunk]
   178     val handler = new DisplayTokenHandler
   179 
   180     var result = Map[Text.Offset, Chunk]()
   181     for (line <- physical_lines) {
   182       out.clear
   183       handler.init(painter.getStyles, font_context, painter, out, margin)
   184       buffer.markTokens(line, handler)
   185 
   186       val line_start = buffer.getLineStartOffset(line)
   187       for (i <- 0 until out.size) {
   188         val chunk = out.get(i)
   189         result += (line_start + chunk.offset -> chunk)
   190       }
   191     }
   192     result
   193   }
   194 
   195   private def paint_chunk_list(gfx: Graphics2D,
   196     offset: Text.Offset, caret_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   197   {
   198     val clip_rect = gfx.getClipBounds
   199     val painter = text_area.getPainter
   200     val font_context = painter.getFontRenderContext
   201 
   202     var w = 0.0f
   203     var chunk_offset = offset
   204     var chunk = head
   205     while (chunk != null) {
   206       val chunk_length = if (chunk.str == null) 0 else chunk.str.length
   207 
   208       if (x + w + chunk.width > clip_rect.x &&
   209           x + w < clip_rect.x + clip_rect.width &&
   210           chunk.accessable && chunk.visible)
   211       {
   212         val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk_length)
   213         val chunk_font = chunk.style.getFont
   214         val chunk_color = chunk.style.getForegroundColor
   215 
   216         val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
   217 
   218         gfx.setFont(chunk_font)
   219         if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
   220             markup.forall(info => info.info.isEmpty) &&
   221             !chunk_range.contains(caret_offset)) {
   222           gfx.setColor(chunk_color)
   223           gfx.drawGlyphVector(chunk.gv, x + w, y)
   224         }
   225         else {
   226           var x1 = x + w
   227           for (Text.Info(range, info) <- markup) {
   228             val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
   229             gfx.setColor(info.getOrElse(chunk_color))
   230             if (range.contains(caret_offset)) {
   231               val astr = new AttributedString(str)
   232               val i = caret_offset - range.start
   233               astr.addAttribute(TextAttribute.FONT, chunk_font)
   234               astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, i + 1)
   235               astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, i + 1)
   236               gfx.drawString(astr.getIterator, x1.toInt, y.toInt)
   237             }
   238             else {
   239               gfx.drawString(str, x1.toInt, y.toInt)
   240             }
   241             x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
   242           }
   243         }
   244       }
   245       w += chunk.width
   246       chunk_offset += chunk_length
   247       chunk = chunk.next.asInstanceOf[Chunk]
   248     }
   249     w
   250   }
   251 
   252   private val text_painter = new TextAreaExtension
   253   {
   254     override def paintScreenLineRange(gfx: Graphics2D,
   255       first_line: Int, last_line: Int, physical_lines: Array[Int],
   256       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   257     {
   258       Isabelle.swing_buffer_lock(buffer) {
   259         val clip = gfx.getClip
   260         val x0 = text_area.getHorizontalOffset
   261         val fm = text_area.getPainter.getFontMetrics
   262         var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
   263 
   264         val caret_offset =
   265           if (text_area.hasFocus) text_area.getCaretPosition
   266           else -1
   267 
   268         val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
   269         for (i <- 0 until physical_lines.length) {
   270           if (physical_lines(i) != -1) {
   271             val x1 =
   272               infos.get(start(i)) match {
   273                 case None => x0
   274                 case Some(chunk) =>
   275                   gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
   276                   val w = paint_chunk_list(gfx, start(i), caret_offset, chunk, x0, y0).toInt
   277                   x0 + w.toInt
   278               }
   279             gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   280             orig_text_painter.paintValidLine(gfx,
   281               first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
   282             orig_caret_painter.paintValidLine(gfx,
   283               first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
   284             gfx.setClip(clip)
   285           }
   286           y0 += line_height
   287         }
   288       }
   289     }
   290   }
   291 
   292 
   293   /* activation */
   294 
   295   def activate()
   296   {
   297     val painter = text_area.getPainter
   298     painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
   299     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   300     painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
   301     painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
   302     painter.removeExtension(orig_text_painter)
   303     painter.removeExtension(orig_caret_painter)
   304   }
   305 
   306   def deactivate()
   307   {
   308     val painter = text_area.getPainter
   309     val caret_layer =
   310       if (painter.isBlockCaretEnabled) TextAreaPainter.BLOCK_CARET_LAYER
   311       else TextAreaPainter.CARET_LAYER
   312     painter.addExtension(caret_layer, orig_caret_painter)
   313     painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   314     painter.removeExtension(reset_snapshot)
   315     painter.removeExtension(text_painter)
   316     painter.removeExtension(background_painter)
   317     painter.removeExtension(set_snapshot)
   318   }
   319 }
   320