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