src/Tools/jEdit/src/text_area_painter.scala
author wenzelm
Tue Aug 23 12:20:12 2011 +0200 (2011-08-23)
changeset 44385 e7fdb008aa7d
parent 44056 be825a69fc67
child 44545 3c40007aa031
permissions -rw-r--r--
propagate editor perspective through document model;
     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       doc_view.robust_body(()) {
    56         painter_snapshot = doc_view.update_snapshot()
    57         painter_clip = gfx.getClip
    58       }
    59     }
    60   }
    61 
    62   private val reset_state = new TextAreaExtension
    63   {
    64     override def paintScreenLineRange(gfx: Graphics2D,
    65       first_line: Int, last_line: Int, physical_lines: Array[Int],
    66       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    67     {
    68       doc_view.robust_body(()) {
    69         painter_snapshot = null
    70         painter_clip = null
    71       }
    72     }
    73   }
    74 
    75 
    76   /* text background */
    77 
    78   private val background_painter = new TextAreaExtension
    79   {
    80     override def paintScreenLineRange(gfx: Graphics2D,
    81       first_line: Int, last_line: Int, physical_lines: Array[Int],
    82       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    83     {
    84       doc_view.robust_body(()) {
    85         val snapshot = painter_snapshot
    86         val ascent = text_area.getPainter.getFontMetrics.getAscent
    87 
    88         for (i <- 0 until physical_lines.length) {
    89           if (physical_lines(i) != -1) {
    90             val line_range = doc_view.proper_line_range(start(i), end(i))
    91 
    92             // background color: status
    93             for {
    94               (command, command_start) <- snapshot.node.command_range(snapshot.revert(line_range))
    95               if !command.is_ignored
    96               range <- line_range.try_restrict(snapshot.convert(command.range + command_start))
    97               r <- Isabelle.gfx_range(text_area, range)
    98               color <- Isabelle_Markup.status_color(snapshot, command)
    99             } {
   100               gfx.setColor(color)
   101               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   102             }
   103 
   104             // background color (1): markup
   105             for {
   106               Text.Info(range, Some(color)) <-
   107                 snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
   108               r <- Isabelle.gfx_range(text_area, range)
   109             } {
   110               gfx.setColor(color)
   111               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   112             }
   113 
   114             // background color (2): markup
   115             for {
   116               Text.Info(range, Some(color)) <-
   117                 snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
   118               r <- Isabelle.gfx_range(text_area, range)
   119             } {
   120               gfx.setColor(color)
   121               gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
   122             }
   123 
   124             // squiggly underline
   125             for {
   126               Text.Info(range, Some(color)) <-
   127                 snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
   128               r <- Isabelle.gfx_range(text_area, range)
   129             } {
   130               gfx.setColor(color)
   131               val x0 = (r.x / 2) * 2
   132               val y0 = r.y + ascent + 1
   133               for (x1 <- Range(x0, x0 + r.length, 2)) {
   134                 val y1 = if (x1 % 4 < 2) y0 else y0 + 1
   135                 gfx.drawLine(x1, y1, x1 + 1, y1)
   136               }
   137             }
   138           }
   139         }
   140       }
   141     }
   142   }
   143 
   144 
   145   /* text */
   146 
   147   def char_width(): Int =
   148   {
   149     val painter = text_area.getPainter
   150     val font = painter.getFont
   151     val font_context = painter.getFontRenderContext
   152     font.getStringBounds(" ", font_context).getWidth.round.toInt
   153   }
   154 
   155   private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
   156   {
   157     val painter = text_area.getPainter
   158     val font = painter.getFont
   159     val font_context = painter.getFontRenderContext
   160 
   161     // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
   162     // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
   163     val margin =
   164       if (buffer.getStringProperty("wrap") != "soft") 0.0f
   165       else {
   166         val max = buffer.getIntegerProperty("maxLineLen", 0)
   167         if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
   168         else painter.getWidth - char_width() * 3
   169       }.toFloat
   170 
   171     val out = new ArrayList[Chunk]
   172     val handler = new DisplayTokenHandler
   173 
   174     var result = Map[Text.Offset, Chunk]()
   175     for (line <- physical_lines) {
   176       out.clear
   177       handler.init(painter.getStyles, font_context, painter, out, margin)
   178       buffer.markTokens(line, handler)
   179 
   180       val line_start = buffer.getLineStartOffset(line)
   181       for (i <- 0 until out.size) {
   182         val chunk = out.get(i)
   183         result += (line_start + chunk.offset -> chunk)
   184       }
   185     }
   186     result
   187   }
   188 
   189   private def paint_chunk_list(
   190     gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   191   {
   192     val clip_rect = gfx.getClipBounds
   193     val painter = text_area.getPainter
   194     val font_context = painter.getFontRenderContext
   195 
   196     var w = 0.0f
   197     var chunk = head
   198     while (chunk != null) {
   199       val chunk_offset = line_start + chunk.offset
   200       if (x + w + chunk.width > clip_rect.x &&
   201           x + w < clip_rect.x + clip_rect.width && chunk.accessable)
   202       {
   203         val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
   204         val chunk_font = chunk.style.getFont
   205         val chunk_color = chunk.style.getForegroundColor
   206 
   207         def string_width(s: String): Float =
   208           if (s.isEmpty) 0.0f
   209           else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
   210 
   211         val caret_range =
   212           if (text_area.hasFocus) doc_view.caret_range()
   213           else Text.Range(-1)
   214 
   215         val markup =
   216           for {
   217             r1 <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color)
   218             r2 <- r1.try_restrict(chunk_range)
   219           } yield r2
   220 
   221         val padded_markup =
   222           if (markup.isEmpty)
   223             Iterator(Text.Info(chunk_range, None))
   224           else
   225             Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
   226             markup.iterator ++
   227             Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
   228 
   229         var x1 = x + w
   230         gfx.setFont(chunk_font)
   231         for (Text.Info(range, info) <- padded_markup if !range.is_singularity) {
   232           val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
   233           gfx.setColor(info.getOrElse(chunk_color))
   234 
   235           range.try_restrict(caret_range) match {
   236             case Some(r) if !r.is_singularity =>
   237               val i = r.start - range.start
   238               val j = r.stop - range.start
   239               val s1 = str.substring(0, i)
   240               val s2 = str.substring(i, j)
   241               val s3 = str.substring(j)
   242 
   243               if (!s1.isEmpty) gfx.drawString(s1, x1, y)
   244 
   245               val astr = new AttributedString(s2)
   246               astr.addAttribute(TextAttribute.FONT, chunk_font)
   247               astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
   248               astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
   249               gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
   250 
   251               if (!s3.isEmpty)
   252                 gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
   253 
   254             case _ =>
   255               gfx.drawString(str, x1, y)
   256           }
   257           x1 += string_width(str)
   258         }
   259       }
   260       w += chunk.width
   261       chunk = chunk.next.asInstanceOf[Chunk]
   262     }
   263     w
   264   }
   265 
   266   private val text_painter = new TextAreaExtension
   267   {
   268     override def paintScreenLineRange(gfx: Graphics2D,
   269       first_line: Int, last_line: Int, physical_lines: Array[Int],
   270       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   271     {
   272       doc_view.robust_body(()) {
   273         val clip = gfx.getClip
   274         val x0 = text_area.getHorizontalOffset
   275         val fm = text_area.getPainter.getFontMetrics
   276         var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
   277 
   278         val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
   279         for (i <- 0 until physical_lines.length) {
   280           if (physical_lines(i) != -1) {
   281             val x1 =
   282               infos.get(start(i)) match {
   283                 case None => x0
   284                 case Some(chunk) =>
   285                   gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
   286                   val w = paint_chunk_list(gfx, start(i), chunk, x0, y0).toInt
   287                   x0 + w.toInt
   288               }
   289             gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   290             orig_text_painter.paintValidLine(gfx,
   291               first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
   292             gfx.setClip(clip)
   293           }
   294           y0 += line_height
   295         }
   296       }
   297     }
   298   }
   299 
   300 
   301   /* foreground */
   302 
   303   private val foreground_painter = new TextAreaExtension
   304   {
   305     override def paintScreenLineRange(gfx: Graphics2D,
   306       first_line: Int, last_line: Int, physical_lines: Array[Int],
   307       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   308     {
   309       doc_view.robust_body(()) {
   310         val snapshot = painter_snapshot
   311 
   312         for (i <- 0 until physical_lines.length) {
   313           if (physical_lines(i) != -1) {
   314             val line_range = doc_view.proper_line_range(start(i), end(i))
   315 
   316             // highlighted range -- potentially from other snapshot
   317             doc_view.highlight_range match {
   318               case Some((range, color)) if line_range.overlaps(range) =>
   319                 Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
   320                   case None =>
   321                   case Some(r) =>
   322                     gfx.setColor(color)
   323                     gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   324                 }
   325               case _ =>
   326             }
   327           }
   328         }
   329       }
   330     }
   331   }
   332 
   333 
   334   /* caret -- outside of text range */
   335 
   336   private class Caret_Painter(before: Boolean) extends TextAreaExtension
   337   {
   338     override def paintValidLine(gfx: Graphics2D,
   339       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   340     {
   341       doc_view.robust_body(()) {
   342         if (before) gfx.clipRect(0, 0, 0, 0)
   343         else gfx.setClip(painter_clip)
   344       }
   345     }
   346   }
   347 
   348   private val before_caret_painter1 = new Caret_Painter(true)
   349   private val after_caret_painter1 = new Caret_Painter(false)
   350   private val before_caret_painter2 = new Caret_Painter(true)
   351   private val after_caret_painter2 = new Caret_Painter(false)
   352 
   353   private val caret_painter = new TextAreaExtension
   354   {
   355     override def paintValidLine(gfx: Graphics2D,
   356       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   357     {
   358       doc_view.robust_body(()) {
   359         if (text_area.hasFocus) {
   360           val caret = text_area.getCaretPosition
   361           if (start <= caret && caret == end - 1) {
   362             val painter = text_area.getPainter
   363             val fm = painter.getFontMetrics
   364 
   365             val offset = caret - text_area.getLineStartOffset(physical_line)
   366             val x = text_area.offsetToXY(physical_line, offset).x
   367             gfx.setColor(painter.getCaretColor)
   368             gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1)
   369           }
   370         }
   371       }
   372     }
   373   }
   374 
   375 
   376   /* activation */
   377 
   378   def activate()
   379   {
   380     val painter = text_area.getPainter
   381     painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
   382     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   383     painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
   384     painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
   385     painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
   386     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
   387     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
   388     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
   389     painter.addExtension(500, foreground_painter)
   390     painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
   391     painter.removeExtension(orig_text_painter)
   392   }
   393 
   394   def deactivate()
   395   {
   396     val painter = text_area.getPainter
   397     painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   398     painter.removeExtension(reset_state)
   399     painter.removeExtension(foreground_painter)
   400     painter.removeExtension(caret_painter)
   401     painter.removeExtension(after_caret_painter2)
   402     painter.removeExtension(before_caret_painter2)
   403     painter.removeExtension(after_caret_painter1)
   404     painter.removeExtension(before_caret_painter1)
   405     painter.removeExtension(text_painter)
   406     painter.removeExtension(background_painter)
   407     painter.removeExtension(set_state)
   408   }
   409 }
   410