separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
authorwenzelm
Sun Jun 12 20:08:49 2011 +0200 (2011-06-12 ago)
changeset 433694c86b3405010
parent 43368 0dc67b3cf8a5
child 43370 1d6ce56e9b2f
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/text_painter.scala
     1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sun Jun 12 16:19:29 2011 +0200
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Jun 12 20:08:49 2011 +0200
     1.3 @@ -23,6 +23,7 @@
     1.4    "src/raw_output_dockable.scala"
     1.5    "src/scala_console.scala"
     1.6    "src/session_dockable.scala"
     1.7 +  "src/text_painter.scala"
     1.8  )
     1.9  
    1.10  declare -a RESOURCES=(
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Jun 12 16:19:29 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sun Jun 12 20:08:49 2011 +0200
     2.3 @@ -17,13 +17,12 @@
     2.4    FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
     2.5  import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
     2.6  import javax.swing.event.{CaretListener, CaretEvent}
     2.7 -import java.util.ArrayList
     2.8  
     2.9  import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
    2.10  import org.gjt.sp.jedit.gui.RolloverButton
    2.11  import org.gjt.sp.jedit.options.GutterOptionPane
    2.12  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    2.13 -import org.gjt.sp.jedit.syntax.{SyntaxStyle, DisplayTokenHandler, Chunk, Token}
    2.14 +import org.gjt.sp.jedit.syntax.{SyntaxStyle}
    2.15  
    2.16  
    2.17  object Document_View
    2.18 @@ -88,52 +87,6 @@
    2.19    }
    2.20  
    2.21  
    2.22 -  /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */
    2.23 -
    2.24 -  def wrap_margin(): Int =
    2.25 -  {
    2.26 -    val buffer = text_area.getBuffer
    2.27 -    val painter = text_area.getPainter
    2.28 -    val font = painter.getFont
    2.29 -    val font_context = painter.getFontRenderContext
    2.30 -
    2.31 -    val soft_wrap = buffer.getStringProperty("wrap") == "soft"
    2.32 -    val max = buffer.getIntegerProperty("maxLineLen", 0)
    2.33 -
    2.34 -    if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
    2.35 -    else if (soft_wrap)
    2.36 -      painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3
    2.37 -    else 0
    2.38 -  }
    2.39 -
    2.40 -
    2.41 -  /* chunks */
    2.42 -
    2.43 -  def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] =
    2.44 -  {
    2.45 -    import scala.collection.JavaConversions._
    2.46 -
    2.47 -    val buffer = text_area.getBuffer
    2.48 -    val painter = text_area.getPainter
    2.49 -    val margin = wrap_margin().toFloat
    2.50 -
    2.51 -    val out = new ArrayList[Chunk]
    2.52 -    val handler = new DisplayTokenHandler
    2.53 -
    2.54 -    var result = Map[Text.Offset, Chunk]()
    2.55 -    for (line <- physical_lines) {
    2.56 -      out.clear
    2.57 -      handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, margin)
    2.58 -      buffer.markTokens(line, handler)
    2.59 -
    2.60 -      val line_start = buffer.getLineStartOffset(line)
    2.61 -      for (chunk <- handler.getChunkList.iterator)
    2.62 -        result += (line_start + chunk.offset -> chunk)
    2.63 -    }
    2.64 -    result
    2.65 -  }
    2.66 -
    2.67 -
    2.68    /* visible line ranges */
    2.69  
    2.70    // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
    2.71 @@ -357,37 +310,7 @@
    2.72      }
    2.73    }
    2.74  
    2.75 -  var use_text_painter = false
    2.76 -
    2.77 -  private val text_painter = new TextAreaExtension
    2.78 -  {
    2.79 -    override def paintScreenLineRange(gfx: Graphics2D,
    2.80 -      first_line: Int, last_line: Int, physical_lines: Array[Int],
    2.81 -      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.82 -    {
    2.83 -      if (use_text_painter) {
    2.84 -        Isabelle.swing_buffer_lock(model.buffer) {
    2.85 -          val painter = text_area.getPainter
    2.86 -          val fm = painter.getFontMetrics
    2.87 -
    2.88 -          val all_chunks = line_chunks(Set[Int]() ++ physical_lines.iterator.filter(i => i != -1))
    2.89 -
    2.90 -          val x0 = text_area.getHorizontalOffset
    2.91 -          var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
    2.92 -          for (i <- 0 until physical_lines.length) {
    2.93 -            if (physical_lines(i) != -1) {
    2.94 -              all_chunks.get(start(i)) match {
    2.95 -                case Some(chunk) =>
    2.96 -                  Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR)
    2.97 -                case None =>
    2.98 -              }
    2.99 -            }
   2.100 -            y0 += line_height
   2.101 -          }
   2.102 -        }
   2.103 -      }
   2.104 -    }
   2.105 -  }
   2.106 +  val text_painter = new Text_Painter(model, text_area)
   2.107  
   2.108    private val gutter_painter = new TextAreaExtension
   2.109    {
   2.110 @@ -558,7 +481,7 @@
   2.111    {
   2.112      val painter = text_area.getPainter
   2.113      painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   2.114 -    painter.addExtension(TextAreaPainter.TEXT_LAYER + 1, text_painter)
   2.115 +    text_painter.activate()
   2.116      text_area.getGutter.addExtension(gutter_painter)
   2.117      text_area.addFocusListener(focus_listener)
   2.118      text_area.getView.addWindowListener(window_listener)
   2.119 @@ -580,7 +503,7 @@
   2.120      text_area.removeCaretListener(caret_listener)
   2.121      text_area.removeLeftOfScrollBar(overview)
   2.122      text_area.getGutter.removeExtension(gutter_painter)
   2.123 -    painter.removeExtension(text_painter)
   2.124 +    text_painter.deactivate()
   2.125      painter.removeExtension(background_painter)
   2.126      exit_popup()
   2.127    }
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/jEdit/src/text_painter.scala	Sun Jun 12 20:08:49 2011 +0200
     3.3 @@ -0,0 +1,128 @@
     3.4 +/*  Title:      Tools/jEdit/src/text_painter.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Replacement painter for jEdit text area.
     3.8 +*/
     3.9 +
    3.10 +package isabelle.jedit
    3.11 +
    3.12 +
    3.13 +import isabelle._
    3.14 +
    3.15 +import java.awt.{Graphics, Graphics2D}
    3.16 +import java.util.ArrayList
    3.17 +
    3.18 +import org.gjt.sp.jedit.Debug
    3.19 +import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
    3.20 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
    3.21 +
    3.22 +
    3.23 +class Text_Painter(model: Document_Model, text_area: JEditTextArea) extends TextAreaExtension
    3.24 +{
    3.25 +  private val orig_text_painter: TextAreaExtension =
    3.26 +  {
    3.27 +    val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText"
    3.28 +    text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
    3.29 +    match {
    3.30 +      case List(x) => x
    3.31 +      case _ => error("Expected exactly one " + name)
    3.32 +    }
    3.33 +  }
    3.34 +
    3.35 +
    3.36 +  /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */
    3.37 +
    3.38 +  private def wrap_margin(): Int =
    3.39 +  {
    3.40 +    val buffer = text_area.getBuffer
    3.41 +    val painter = text_area.getPainter
    3.42 +    val font = painter.getFont
    3.43 +    val font_context = painter.getFontRenderContext
    3.44 +
    3.45 +    val soft_wrap = buffer.getStringProperty("wrap") == "soft"
    3.46 +    val max = buffer.getIntegerProperty("maxLineLen", 0)
    3.47 +
    3.48 +    if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
    3.49 +    else if (soft_wrap)
    3.50 +      painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3
    3.51 +    else 0
    3.52 +  }
    3.53 +
    3.54 +
    3.55 +  /* chunks */
    3.56 +
    3.57 +  private def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] =
    3.58 +  {
    3.59 +    import scala.collection.JavaConversions._
    3.60 +
    3.61 +    val buffer = text_area.getBuffer
    3.62 +    val painter = text_area.getPainter
    3.63 +    val margin = wrap_margin().toFloat
    3.64 +
    3.65 +    val out = new ArrayList[Chunk]
    3.66 +    val handler = new DisplayTokenHandler
    3.67 +
    3.68 +    var result = Map[Text.Offset, Chunk]()
    3.69 +    for (line <- physical_lines) {
    3.70 +      out.clear
    3.71 +      handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, margin)
    3.72 +      buffer.markTokens(line, handler)
    3.73 +
    3.74 +      val line_start = buffer.getLineStartOffset(line)
    3.75 +      for (chunk <- handler.getChunkList.iterator)
    3.76 +        result += (line_start + chunk.offset -> chunk)
    3.77 +    }
    3.78 +    result
    3.79 +  }
    3.80 +
    3.81 +
    3.82 +  var use = false
    3.83 +
    3.84 +  override def paintScreenLineRange(gfx: Graphics2D,
    3.85 +    first_line: Int, last_line: Int, physical_lines: Array[Int],
    3.86 +    start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    3.87 +  {
    3.88 +    if (use) {
    3.89 +      Isabelle.swing_buffer_lock(model.buffer) {
    3.90 +        val painter = text_area.getPainter
    3.91 +        val fm = painter.getFontMetrics
    3.92 +
    3.93 +        val all_chunks = line_chunks(Set[Int]() ++ physical_lines.iterator.filter(i => i != -1))
    3.94 +
    3.95 +        val x0 = text_area.getHorizontalOffset
    3.96 +        var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
    3.97 +        for (i <- 0 until physical_lines.length) {
    3.98 +          if (physical_lines(i) != -1) {
    3.99 +            all_chunks.get(start(i)) match {
   3.100 +              case Some(chunk) =>
   3.101 +                Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR)
   3.102 +              case None =>
   3.103 +            }
   3.104 +          }
   3.105 +          y0 += line_height
   3.106 +        }
   3.107 +      }
   3.108 +    }
   3.109 +    else
   3.110 +      orig_text_painter.paintScreenLineRange(
   3.111 +        gfx, first_line, last_line, physical_lines, start, end, y, line_height)
   3.112 +  }
   3.113 +
   3.114 +
   3.115 +  /* activation */
   3.116 +
   3.117 +  def activate()
   3.118 +  {
   3.119 +    val painter = text_area.getPainter
   3.120 +    painter.removeExtension(orig_text_painter)
   3.121 +    painter.addExtension(TextAreaPainter.TEXT_LAYER, this)
   3.122 +  }
   3.123 +
   3.124 +  def deactivate()
   3.125 +  {
   3.126 +    val painter = text_area.getPainter
   3.127 +    painter.removeExtension(this)
   3.128 +    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   3.129 +  }
   3.130 +}
   3.131 +