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