some direct text foreground painting, instead of token marking;
authorwenzelm
Mon Jun 13 23:09:01 2011 +0200 (2011-06-13 ago)
changeset 433760f6880c1c759
parent 43375 09d992ab57c6
child 43377 ba199d75bc7e
some direct text foreground painting, instead of token marking;
common snapshot for all text area painters (NOT gutter etc.)
tuned;
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle_markup.scala
src/Tools/jEdit/src/text_painter.scala
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Jun 13 14:22:33 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Jun 13 23:09:01 2011 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4  }
     1.5  
     1.6  
     1.7 -class Document_View(val model: Document_Model, text_area: JEditTextArea)
     1.8 +class Document_View(val model: Document_Model, val text_area: JEditTextArea)
     1.9  {
    1.10    private val session = model.session
    1.11  
    1.12 @@ -207,7 +207,35 @@
    1.13    }
    1.14  
    1.15  
    1.16 -  /* TextArea painters */
    1.17 +  /* TextArea painting */
    1.18 +
    1.19 +  @volatile private var _text_area_snapshot: Option[Document.Snapshot] = None
    1.20 +
    1.21 +  def text_area_snapshot(): Document.Snapshot =
    1.22 +    _text_area_snapshot match {
    1.23 +      case Some(snapshot) => snapshot
    1.24 +      case None => error("Missing text area snapshot")
    1.25 +    }
    1.26 +
    1.27 +  private val set_snapshot = new TextAreaExtension
    1.28 +  {
    1.29 +    override def paintScreenLineRange(gfx: Graphics2D,
    1.30 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.31 +      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.32 +    {
    1.33 +      _text_area_snapshot = Some(model.snapshot())
    1.34 +    }
    1.35 +  }
    1.36 +
    1.37 +  private val reset_snapshot = new TextAreaExtension
    1.38 +  {
    1.39 +    override def paintScreenLineRange(gfx: Graphics2D,
    1.40 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.41 +      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.42 +    {
    1.43 +      _text_area_snapshot = None
    1.44 +    }
    1.45 +  }
    1.46  
    1.47    private val background_painter = new TextAreaExtension
    1.48    {
    1.49 @@ -216,7 +244,7 @@
    1.50        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.51      {
    1.52        Isabelle.swing_buffer_lock(model.buffer) {
    1.53 -        val snapshot = model.snapshot()
    1.54 +        val snapshot = text_area_snapshot()
    1.55          val ascent = text_area.getPainter.getFontMetrics.getAscent
    1.56  
    1.57          for (i <- 0 until physical_lines.length) {
    1.58 @@ -310,7 +338,10 @@
    1.59      }
    1.60    }
    1.61  
    1.62 -  val text_painter = new Text_Painter(model, text_area)
    1.63 +  val text_painter = new Text_Painter(this)
    1.64 +
    1.65 +
    1.66 +  /* Gutter painting */
    1.67  
    1.68    private val gutter_painter = new TextAreaExtension
    1.69    {
    1.70 @@ -480,8 +511,12 @@
    1.71    private def activate()
    1.72    {
    1.73      val painter = text_area.getPainter
    1.74 +
    1.75 +    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
    1.76      painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
    1.77      text_painter.activate()
    1.78 +    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
    1.79 +
    1.80      text_area.getGutter.addExtension(gutter_painter)
    1.81      text_area.addFocusListener(focus_listener)
    1.82      text_area.getView.addWindowListener(window_listener)
    1.83 @@ -495,6 +530,7 @@
    1.84    private def deactivate()
    1.85    {
    1.86      val painter = text_area.getPainter
    1.87 +
    1.88      session.commands_changed -= main_actor
    1.89      session.global_settings -= main_actor
    1.90      text_area.removeFocusListener(focus_listener)
    1.91 @@ -503,8 +539,11 @@
    1.92      text_area.removeCaretListener(caret_listener)
    1.93      text_area.removeLeftOfScrollBar(overview)
    1.94      text_area.getGutter.removeExtension(gutter_painter)
    1.95 +
    1.96 +    painter.removeExtension(reset_snapshot)
    1.97      text_painter.deactivate()
    1.98      painter.removeExtension(background_painter)
    1.99 +    painter.removeExtension(set_snapshot)
   1.100      exit_popup()
   1.101    }
   1.102  }
     2.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Mon Jun 13 14:22:33 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Mon Jun 13 23:09:01 2011 +0200
     2.3 @@ -28,6 +28,10 @@
     2.4    val bad_color = new Color(255, 106, 106, 100)
     2.5    val hilite_color = new Color(255, 204, 102, 100)
     2.6  
     2.7 +  val free_color = new Color(0, 0, 0xFF)
     2.8 +  val skolem_color = new Color(0xD2, 0x69, 0x1E)
     2.9 +  val bound_color = new Color(0, 0x8B, 0)
    2.10 +
    2.11    class Icon(val priority: Int, val icon: javax.swing.Icon)
    2.12    {
    2.13      def >= (that: Icon): Boolean = this.priority >= that.priority
    2.14 @@ -100,6 +104,13 @@
    2.15      case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
    2.16    }
    2.17  
    2.18 +  val foreground: Markup_Tree.Select[Color] =
    2.19 +  {
    2.20 +    case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => free_color
    2.21 +    case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => skolem_color
    2.22 +    case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => bound_color
    2.23 +  }
    2.24 +
    2.25    val tooltip: Markup_Tree.Select[String] =
    2.26    {
    2.27      case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\""
    2.28 @@ -157,10 +168,10 @@
    2.29        Markup.DYNAMIC_FACT -> LABEL,
    2.30        // inner syntax
    2.31        Markup.TFREE -> NULL,
    2.32 -      Markup.FREE -> MARKUP,
    2.33 +      Markup.FREE -> NULL,
    2.34        Markup.TVAR -> NULL,
    2.35 -      Markup.SKOLEM -> COMMENT2,
    2.36 -      Markup.BOUND -> LABEL,
    2.37 +      Markup.SKOLEM -> NULL,
    2.38 +      Markup.BOUND -> NULL,
    2.39        Markup.VAR -> NULL,
    2.40        Markup.NUM -> DIGIT,
    2.41        Markup.FLOAT -> DIGIT,
     3.1 --- a/src/Tools/jEdit/src/text_painter.scala	Mon Jun 13 14:22:33 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/text_painter.scala	Mon Jun 13 23:09:01 2011 +0200
     3.3 @@ -17,8 +17,10 @@
     3.4  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
     3.5  
     3.6  
     3.7 -class Text_Painter(model: Document_Model, text_area: JEditTextArea) extends TextAreaExtension
     3.8 +class Text_Painter(doc_view: Document_View) extends TextAreaExtension
     3.9  {
    3.10 +  private val text_area = doc_view.text_area
    3.11 +
    3.12    private val orig_text_painter: TextAreaExtension =
    3.13    {
    3.14      val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText"
    3.15 @@ -33,35 +35,56 @@
    3.16      first_line: Int, last_line: Int, physical_lines: Array[Int],
    3.17      start: Array[Int], end: Array[Int], y_start: Int, line_height: Int)
    3.18    {
    3.19 -    def paint_chunk_list(head: Chunk, x: Float, y: Float): Float =
    3.20 -    {
    3.21 -      val clip_rect = gfx.getClipBounds
    3.22 -      var w = 0.0f
    3.23 -      var chunk = head
    3.24 -      while (chunk != null) {
    3.25 -        if (x + w + chunk.width > clip_rect.x &&
    3.26 -            x + w < clip_rect.x + clip_rect.width &&
    3.27 -            chunk.accessable && chunk.visible)
    3.28 -        {
    3.29 -          gfx.setFont(chunk.style.getFont)
    3.30 -          gfx.setColor(chunk.style.getForegroundColor)
    3.31 -          if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null)
    3.32 -            gfx.drawGlyphVector(chunk.gv, x + w, y)
    3.33 -          else if (chunk.str != null)
    3.34 -            gfx.drawString(chunk.str, (x + w).toInt, y.toInt)
    3.35 -        }
    3.36 -        w += chunk.width
    3.37 -        chunk = chunk.next.asInstanceOf[Chunk]
    3.38 -      }
    3.39 -      w
    3.40 -    }
    3.41 -
    3.42      val buffer = text_area.getBuffer
    3.43      Isabelle.swing_buffer_lock(buffer) {
    3.44        val painter = text_area.getPainter
    3.45        val font = painter.getFont
    3.46        val font_context = painter.getFontRenderContext
    3.47 -      val fm = painter.getFontMetrics
    3.48 +      val font_metrics = painter.getFontMetrics
    3.49 +
    3.50 +      def paint_chunk_list(head_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
    3.51 +      {
    3.52 +        val clip_rect = gfx.getClipBounds
    3.53 +
    3.54 +        var w = 0.0f
    3.55 +        var offset = head_offset
    3.56 +        var chunk = head
    3.57 +        while (chunk != null) {
    3.58 +          val chunk_length = if (chunk.str == null) 0 else chunk.str.length
    3.59 +
    3.60 +          if (x + w + chunk.width > clip_rect.x &&
    3.61 +              x + w < clip_rect.x + clip_rect.width &&
    3.62 +              chunk.accessable && chunk.visible)
    3.63 +          {
    3.64 +            val chunk_range = Text.Range(offset, offset + chunk_length)
    3.65 +            val chunk_font = chunk.style.getFont
    3.66 +            val chunk_color = chunk.style.getForegroundColor
    3.67 +
    3.68 +            val markup =
    3.69 +              doc_view.text_area_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
    3.70 +
    3.71 +            gfx.setFont(chunk_font)
    3.72 +            if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
    3.73 +                markup.forall(info => info.info.isEmpty)) {
    3.74 +              gfx.setColor(chunk_color)
    3.75 +              gfx.drawGlyphVector(chunk.gv, x + w, y)
    3.76 +            }
    3.77 +            else {
    3.78 +              var xpos = x + w
    3.79 +              for (Text.Info(range, info) <- markup) {
    3.80 +                val str = chunk.str.substring(range.start - offset, range.stop - offset)
    3.81 +                gfx.setColor(info.getOrElse(chunk_color))
    3.82 +                gfx.drawString(str, xpos.toInt, y.toInt)
    3.83 +                xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
    3.84 +              }
    3.85 +            }
    3.86 +          }
    3.87 +          w += chunk.width
    3.88 +          offset += chunk_length
    3.89 +          chunk = chunk.next.asInstanceOf[Chunk]
    3.90 +        }
    3.91 +        w
    3.92 +      }
    3.93  
    3.94        // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
    3.95        // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
    3.96 @@ -98,12 +121,14 @@
    3.97  
    3.98        val clip = gfx.getClip
    3.99        val x0 = text_area.getHorizontalOffset
   3.100 -      var y0 = y_start + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
   3.101 +      var y0 =
   3.102 +        y_start + font_metrics.getHeight - (font_metrics.getLeading + 1) - font_metrics.getDescent
   3.103 +
   3.104        for (i <- 0 until physical_lines.length) {
   3.105          if (physical_lines(i) != -1) {
   3.106            line_infos.get(start(i)) match {
   3.107              case Some(chunk) =>
   3.108 -              val w = paint_chunk_list(chunk, x0, y0).toInt
   3.109 +              val w = paint_chunk_list(start(i), chunk, x0, y0).toInt
   3.110                gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   3.111                orig_text_painter.paintValidLine(gfx,
   3.112                  first_line + i, physical_lines(i), start(i), end(i), y_start + line_height * i)