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