wenzelm@43381: /*  Title:      Tools/jEdit/src/text_area_painter.scala
wenzelm@43369:     Author:     Makarius
wenzelm@43369: 
wenzelm@43381: Painter setup for main jEdit text area.
wenzelm@43369: */
wenzelm@43369: 
wenzelm@43369: package isabelle.jedit
wenzelm@43369: 
wenzelm@43369: 
wenzelm@43369: import isabelle._
wenzelm@43369: 
wenzelm@43393: import java.awt.{Graphics2D, Shape}
wenzelm@43392: import java.awt.font.TextAttribute
wenzelm@43392: import java.text.AttributedString
wenzelm@43369: import java.util.ArrayList
wenzelm@43369: 
wenzelm@43369: import org.gjt.sp.jedit.Debug
wenzelm@43369: import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
wenzelm@43392: import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, JEditTextArea}
wenzelm@43369: 
wenzelm@43369: 
wenzelm@43381: class Text_Area_Painter(doc_view: Document_View)
wenzelm@43369: {
wenzelm@43381:   private val model = doc_view.model
wenzelm@43382:   private val buffer = model.buffer
wenzelm@43376:   private val text_area = doc_view.text_area
wenzelm@43376: 
wenzelm@43392: 
wenzelm@43392:   /* original painters */
wenzelm@43392: 
wenzelm@43392:   private def pick_extension(name: String): TextAreaExtension =
wenzelm@43369:   {
wenzelm@43369:     text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
wenzelm@43369:     match {
wenzelm@43369:       case List(x) => x
wenzelm@43369:       case _ => error("Expected exactly one " + name)
wenzelm@43369:     }
wenzelm@43369:   }
wenzelm@43369: 
wenzelm@43392:   private val orig_text_painter =
wenzelm@43392:     pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
wenzelm@43392: 
wenzelm@43392: 
wenzelm@43393:   /* common painter state */
wenzelm@43381: 
wenzelm@43393:   @volatile private var painter_snapshot: Document.Snapshot = null
wenzelm@43393:   @volatile private var painter_clip: Shape = null
wenzelm@43381: 
wenzelm@43393:   private val set_state = new TextAreaExtension
wenzelm@43381:   {
wenzelm@43381:     override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381:       first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381:       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381:     {
wenzelm@43404:       doc_view.robust_body(()) {
wenzelm@43419:         painter_snapshot = doc_view.update_snapshot()
wenzelm@43404:         painter_clip = gfx.getClip
wenzelm@43404:       }
wenzelm@43381:     }
wenzelm@43381:   }
wenzelm@43381: 
wenzelm@43393:   private val reset_state = new TextAreaExtension
wenzelm@43369:   {
wenzelm@43381:     override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381:       first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381:       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381:     {
wenzelm@43404:       doc_view.robust_body(()) {
wenzelm@43404:         painter_snapshot = null
wenzelm@43404:         painter_clip = null
wenzelm@43404:       }
wenzelm@43381:     }
wenzelm@43381:   }
wenzelm@43381: 
wenzelm@43381: 
wenzelm@43381:   /* text background */
wenzelm@43376: 
wenzelm@43381:   private val background_painter = new TextAreaExtension
wenzelm@43381:   {
wenzelm@43381:     override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381:       first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43381:       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381:     {
wenzelm@43404:       doc_view.robust_body(()) {
wenzelm@43393:         val snapshot = painter_snapshot
wenzelm@43381:         val ascent = text_area.getPainter.getFontMetrics.getAscent
wenzelm@43376: 
wenzelm@43381:         for (i <- 0 until physical_lines.length) {
wenzelm@43381:           if (physical_lines(i) != -1) {
wenzelm@43381:             val line_range = doc_view.proper_line_range(start(i), end(i))
wenzelm@43376: 
wenzelm@43381:             // background color: status
wenzelm@43381:             for {
wenzelm@43428:               (command, command_start) <- snapshot.node.command_range(snapshot.revert(line_range))
wenzelm@43428:               if !command.is_ignored
wenzelm@43428:               range <- line_range.try_restrict(snapshot.convert(command.range + command_start))
wenzelm@43381:               r <- Isabelle.gfx_range(text_area, range)
wenzelm@43381:               color <- Isabelle_Markup.status_color(snapshot, command)
wenzelm@43381:             } {
wenzelm@43381:               gfx.setColor(color)
wenzelm@43381:               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@43381:             }
wenzelm@43376: 
wenzelm@43381:             // background color (1): markup
wenzelm@43381:             for {
wenzelm@43381:               Text.Info(range, Some(color)) <-
wenzelm@43381:                 snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
wenzelm@43381:               r <- Isabelle.gfx_range(text_area, range)
wenzelm@43381:             } {
wenzelm@43381:               gfx.setColor(color)
wenzelm@43381:               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@43381:             }
wenzelm@43376: 
wenzelm@43381:             // background color (2): markup
wenzelm@43381:             for {
wenzelm@43381:               Text.Info(range, Some(color)) <-
wenzelm@43381:                 snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
wenzelm@43381:               r <- Isabelle.gfx_range(text_area, range)
wenzelm@43381:             } {
wenzelm@43381:               gfx.setColor(color)
wenzelm@43381:               gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
wenzelm@43376:             }
wenzelm@43381: 
wenzelm@43381:             // squiggly underline
wenzelm@43381:             for {
wenzelm@43381:               Text.Info(range, Some(color)) <-
wenzelm@43381:                 snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
wenzelm@43381:               r <- Isabelle.gfx_range(text_area, range)
wenzelm@43381:             } {
wenzelm@43381:               gfx.setColor(color)
wenzelm@43381:               val x0 = (r.x / 2) * 2
wenzelm@43381:               val y0 = r.y + ascent + 1
wenzelm@43381:               for (x1 <- Range(x0, x0 + r.length, 2)) {
wenzelm@43381:                 val y1 = if (x1 % 4 < 2) y0 else y0 + 1
wenzelm@43381:                 gfx.drawLine(x1, y1, x1 + 1, y1)
wenzelm@43376:               }
wenzelm@43376:             }
wenzelm@43376:           }
wenzelm@43376:         }
wenzelm@43376:       }
wenzelm@43381:     }
wenzelm@43381:   }
wenzelm@43381: 
wenzelm@43381: 
wenzelm@43381:   /* text */
wenzelm@43369: 
wenzelm@43393:   def char_width(): Int =
wenzelm@43393:   {
wenzelm@43393:     val painter = text_area.getPainter
wenzelm@43393:     val font = painter.getFont
wenzelm@43393:     val font_context = painter.getFontRenderContext
wenzelm@43393:     font.getStringBounds(" ", font_context).getWidth.round.toInt
wenzelm@43393:   }
wenzelm@43393: 
wenzelm@43382:   private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
wenzelm@43382:   {
wenzelm@43382:     val painter = text_area.getPainter
wenzelm@43382:     val font = painter.getFont
wenzelm@43382:     val font_context = painter.getFontRenderContext
wenzelm@43382: 
wenzelm@43382:     // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
wenzelm@43382:     // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
wenzelm@43382:     val margin =
wenzelm@43382:       if (buffer.getStringProperty("wrap") != "soft") 0.0f
wenzelm@43382:       else {
wenzelm@43382:         val max = buffer.getIntegerProperty("maxLineLen", 0)
wenzelm@43382:         if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
wenzelm@43393:         else painter.getWidth - char_width() * 3
wenzelm@43382:       }.toFloat
wenzelm@43382: 
wenzelm@43382:     val out = new ArrayList[Chunk]
wenzelm@43382:     val handler = new DisplayTokenHandler
wenzelm@43382: 
wenzelm@43382:     var result = Map[Text.Offset, Chunk]()
wenzelm@43382:     for (line <- physical_lines) {
wenzelm@43382:       out.clear
wenzelm@43382:       handler.init(painter.getStyles, font_context, painter, out, margin)
wenzelm@43382:       buffer.markTokens(line, handler)
wenzelm@43382: 
wenzelm@43382:       val line_start = buffer.getLineStartOffset(line)
wenzelm@43382:       for (i <- 0 until out.size) {
wenzelm@43382:         val chunk = out.get(i)
wenzelm@43382:         result += (line_start + chunk.offset -> chunk)
wenzelm@43382:       }
wenzelm@43382:     }
wenzelm@43382:     result
wenzelm@43382:   }
wenzelm@43382: 
wenzelm@43382:   private def paint_chunk_list(gfx: Graphics2D,
wenzelm@43392:     offset: Text.Offset, caret_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
wenzelm@43382:   {
wenzelm@43382:     val clip_rect = gfx.getClipBounds
wenzelm@43392:     val painter = text_area.getPainter
wenzelm@43392:     val font_context = painter.getFontRenderContext
wenzelm@43382: 
wenzelm@43382:     var w = 0.0f
wenzelm@43382:     var chunk_offset = offset
wenzelm@43382:     var chunk = head
wenzelm@43382:     while (chunk != null) {
wenzelm@43382:       val chunk_length = if (chunk.str == null) 0 else chunk.str.length
wenzelm@43382: 
wenzelm@43382:       if (x + w + chunk.width > clip_rect.x &&
wenzelm@43382:           x + w < clip_rect.x + clip_rect.width &&
wenzelm@43382:           chunk.accessable && chunk.visible)
wenzelm@43382:       {
wenzelm@43382:         val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk_length)
wenzelm@43382:         val chunk_font = chunk.style.getFont
wenzelm@43382:         val chunk_color = chunk.style.getForegroundColor
wenzelm@43382: 
wenzelm@43426:         val markup =
wenzelm@43428:           for {
wenzelm@43434:             x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color)
wenzelm@43428:             y <- x.try_restrict(chunk_range)
wenzelm@43428:           } yield y
wenzelm@43382: 
wenzelm@43382:         gfx.setFont(chunk_font)
wenzelm@43382:         if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
wenzelm@43392:             markup.forall(info => info.info.isEmpty) &&
wenzelm@43392:             !chunk_range.contains(caret_offset)) {
wenzelm@43382:           gfx.setColor(chunk_color)
wenzelm@43382:           gfx.drawGlyphVector(chunk.gv, x + w, y)
wenzelm@43382:         }
wenzelm@43426:         else if (!markup.isEmpty) {
wenzelm@43383:           var x1 = x + w
wenzelm@43426:           for {
wenzelm@43428:             Text.Info(range, info) <-
wenzelm@43426:               Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
wenzelm@43426:               markup.iterator ++
wenzelm@43426:               Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
wenzelm@43426:             if !range.is_singularity
wenzelm@43426:           } {
wenzelm@43426:             val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
wenzelm@43382:             gfx.setColor(info.getOrElse(chunk_color))
wenzelm@43392:             if (range.contains(caret_offset)) {
wenzelm@43392:               val astr = new AttributedString(str)
wenzelm@43392:               val i = caret_offset - range.start
wenzelm@43392:               astr.addAttribute(TextAttribute.FONT, chunk_font)
wenzelm@43392:               astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, i + 1)
wenzelm@43392:               astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, i + 1)
wenzelm@43392:               gfx.drawString(astr.getIterator, x1.toInt, y.toInt)
wenzelm@43392:             }
wenzelm@43392:             else {
wenzelm@43392:               gfx.drawString(str, x1.toInt, y.toInt)
wenzelm@43392:             }
wenzelm@43383:             x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
wenzelm@43382:           }
wenzelm@43382:         }
wenzelm@43382:       }
wenzelm@43382:       w += chunk.width
wenzelm@43382:       chunk_offset += chunk_length
wenzelm@43382:       chunk = chunk.next.asInstanceOf[Chunk]
wenzelm@43382:     }
wenzelm@43382:     w
wenzelm@43382:   }
wenzelm@43382: 
wenzelm@43381:   private val text_painter = new TextAreaExtension
wenzelm@43381:   {
wenzelm@43381:     override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43381:       first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43382:       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43381:     {
wenzelm@43404:       doc_view.robust_body(()) {
wenzelm@43381:         val clip = gfx.getClip
wenzelm@43381:         val x0 = text_area.getHorizontalOffset
wenzelm@43382:         val fm = text_area.getPainter.getFontMetrics
wenzelm@43382:         var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
wenzelm@43372: 
wenzelm@43392:         val caret_offset =
wenzelm@43392:           if (text_area.hasFocus) text_area.getCaretPosition
wenzelm@43392:           else -1
wenzelm@43392: 
wenzelm@43382:         val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
wenzelm@43381:         for (i <- 0 until physical_lines.length) {
wenzelm@43381:           if (physical_lines(i) != -1) {
wenzelm@43392:             val x1 =
wenzelm@43392:               infos.get(start(i)) match {
wenzelm@43392:                 case None => x0
wenzelm@43392:                 case Some(chunk) =>
wenzelm@43392:                   gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
wenzelm@43392:                   val w = paint_chunk_list(gfx, start(i), caret_offset, chunk, x0, y0).toInt
wenzelm@43392:                   x0 + w.toInt
wenzelm@43392:               }
wenzelm@43392:             gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
wenzelm@43392:             orig_text_painter.paintValidLine(gfx,
wenzelm@43392:               first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
wenzelm@43392:             gfx.setClip(clip)
wenzelm@43369:           }
wenzelm@43381:           y0 += line_height
wenzelm@43369:         }
wenzelm@43369:       }
wenzelm@43369:     }
wenzelm@43369:   }
wenzelm@43369: 
wenzelm@43369: 
wenzelm@43435:   /* foreground */
wenzelm@43435: 
wenzelm@43435:   private val foreground_painter = new TextAreaExtension
wenzelm@43435:   {
wenzelm@43435:     override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@43435:       first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@43435:       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@43435:     {
wenzelm@43435:       doc_view.robust_body(()) {
wenzelm@43435:         val snapshot = painter_snapshot
wenzelm@43435: 
wenzelm@43435:         for (i <- 0 until physical_lines.length) {
wenzelm@43435:           if (physical_lines(i) != -1) {
wenzelm@43435:             val line_range = doc_view.proper_line_range(start(i), end(i))
wenzelm@43435: 
wenzelm@43435:             // highlighted range -- potentially from other snapshot
wenzelm@43435:             doc_view.highlight_range match {
wenzelm@43435:               case Some((range, color)) if line_range.overlaps(range) =>
wenzelm@43435:                 Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
wenzelm@43435:                   case None =>
wenzelm@43435:                   case Some(r) =>
wenzelm@43435:                     gfx.setColor(color)
wenzelm@43435:                     gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@43435:                 }
wenzelm@43435:               case _ =>
wenzelm@43435:             }
wenzelm@43435:           }
wenzelm@43435:         }
wenzelm@43435:       }
wenzelm@43435:     }
wenzelm@43435:   }
wenzelm@43435: 
wenzelm@43435: 
wenzelm@43393:   /* caret -- outside of text range */
wenzelm@43393: 
wenzelm@43393:   private class Caret_Painter(before: Boolean) extends TextAreaExtension
wenzelm@43393:   {
wenzelm@43393:     override def paintValidLine(gfx: Graphics2D,
wenzelm@43393:       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
wenzelm@43393:     {
wenzelm@43404:       doc_view.robust_body(()) {
wenzelm@43404:         if (before) gfx.clipRect(0, 0, 0, 0)
wenzelm@43404:         else gfx.setClip(painter_clip)
wenzelm@43404:       }
wenzelm@43393:     }
wenzelm@43393:   }
wenzelm@43393: 
wenzelm@43393:   private val before_caret_painter1 = new Caret_Painter(true)
wenzelm@43393:   private val after_caret_painter1 = new Caret_Painter(false)
wenzelm@43393:   private val before_caret_painter2 = new Caret_Painter(true)
wenzelm@43393:   private val after_caret_painter2 = new Caret_Painter(false)
wenzelm@43393: 
wenzelm@43393:   private val caret_painter = new TextAreaExtension
wenzelm@43393:   {
wenzelm@43393:     override def paintValidLine(gfx: Graphics2D,
wenzelm@43393:       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
wenzelm@43393:     {
wenzelm@43404:       doc_view.robust_body(()) {
wenzelm@43398:         if (text_area.hasFocus) {
wenzelm@43398:           val caret = text_area.getCaretPosition
wenzelm@43398:           if (start <= caret && caret == end - 1) {
wenzelm@43398:             val painter = text_area.getPainter
wenzelm@43398:             val fm = painter.getFontMetrics
wenzelm@43393: 
wenzelm@43398:             val offset = caret - text_area.getLineStartOffset(physical_line)
wenzelm@43398:             val x = text_area.offsetToXY(physical_line, offset).x
wenzelm@43398:             gfx.setColor(painter.getCaretColor)
wenzelm@43398:             gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1)
wenzelm@43398:           }
wenzelm@43393:         }
wenzelm@43393:       }
wenzelm@43393:     }
wenzelm@43393:   }
wenzelm@43393: 
wenzelm@43393: 
wenzelm@43369:   /* activation */
wenzelm@43369: 
wenzelm@43369:   def activate()
wenzelm@43369:   {
wenzelm@43369:     val painter = text_area.getPainter
wenzelm@43393:     painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
wenzelm@43381:     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
wenzelm@43381:     painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
wenzelm@43393:     painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
wenzelm@43393:     painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
wenzelm@43393:     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
wenzelm@43393:     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
wenzelm@43393:     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
wenzelm@43435:     painter.addExtension(500, foreground_painter)
wenzelm@43393:     painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
wenzelm@43369:     painter.removeExtension(orig_text_painter)
wenzelm@43369:   }
wenzelm@43369: 
wenzelm@43369:   def deactivate()
wenzelm@43369:   {
wenzelm@43369:     val painter = text_area.getPainter
wenzelm@43396:     painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
wenzelm@43393:     painter.removeExtension(reset_state)
wenzelm@43435:     painter.removeExtension(foreground_painter)
wenzelm@43393:     painter.removeExtension(caret_painter)
wenzelm@43393:     painter.removeExtension(after_caret_painter2)
wenzelm@43393:     painter.removeExtension(before_caret_painter2)
wenzelm@43393:     painter.removeExtension(after_caret_painter1)
wenzelm@43393:     painter.removeExtension(before_caret_painter1)
wenzelm@43381:     painter.removeExtension(text_painter)
wenzelm@43381:     painter.removeExtension(background_painter)
wenzelm@43393:     painter.removeExtension(set_state)
wenzelm@43369:   }
wenzelm@43369: }
wenzelm@43369: