src/Tools/jEdit/src/document_view.scala
changeset 43369 4c86b3405010
parent 43282 5d294220ca43
child 43376 0f6880c1c759
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Jun 12 16:19:29 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sun Jun 12 20:08:49 2011 +0200
     1.3 @@ -17,13 +17,12 @@
     1.4    FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
     1.5  import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
     1.6  import javax.swing.event.{CaretListener, CaretEvent}
     1.7 -import java.util.ArrayList
     1.8  
     1.9  import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
    1.10  import org.gjt.sp.jedit.gui.RolloverButton
    1.11  import org.gjt.sp.jedit.options.GutterOptionPane
    1.12  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    1.13 -import org.gjt.sp.jedit.syntax.{SyntaxStyle, DisplayTokenHandler, Chunk, Token}
    1.14 +import org.gjt.sp.jedit.syntax.{SyntaxStyle}
    1.15  
    1.16  
    1.17  object Document_View
    1.18 @@ -88,52 +87,6 @@
    1.19    }
    1.20  
    1.21  
    1.22 -  /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */
    1.23 -
    1.24 -  def wrap_margin(): Int =
    1.25 -  {
    1.26 -    val buffer = text_area.getBuffer
    1.27 -    val painter = text_area.getPainter
    1.28 -    val font = painter.getFont
    1.29 -    val font_context = painter.getFontRenderContext
    1.30 -
    1.31 -    val soft_wrap = buffer.getStringProperty("wrap") == "soft"
    1.32 -    val max = buffer.getIntegerProperty("maxLineLen", 0)
    1.33 -
    1.34 -    if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
    1.35 -    else if (soft_wrap)
    1.36 -      painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3
    1.37 -    else 0
    1.38 -  }
    1.39 -
    1.40 -
    1.41 -  /* chunks */
    1.42 -
    1.43 -  def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] =
    1.44 -  {
    1.45 -    import scala.collection.JavaConversions._
    1.46 -
    1.47 -    val buffer = text_area.getBuffer
    1.48 -    val painter = text_area.getPainter
    1.49 -    val margin = wrap_margin().toFloat
    1.50 -
    1.51 -    val out = new ArrayList[Chunk]
    1.52 -    val handler = new DisplayTokenHandler
    1.53 -
    1.54 -    var result = Map[Text.Offset, Chunk]()
    1.55 -    for (line <- physical_lines) {
    1.56 -      out.clear
    1.57 -      handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, margin)
    1.58 -      buffer.markTokens(line, handler)
    1.59 -
    1.60 -      val line_start = buffer.getLineStartOffset(line)
    1.61 -      for (chunk <- handler.getChunkList.iterator)
    1.62 -        result += (line_start + chunk.offset -> chunk)
    1.63 -    }
    1.64 -    result
    1.65 -  }
    1.66 -
    1.67 -
    1.68    /* visible line ranges */
    1.69  
    1.70    // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
    1.71 @@ -357,37 +310,7 @@
    1.72      }
    1.73    }
    1.74  
    1.75 -  var use_text_painter = false
    1.76 -
    1.77 -  private val text_painter = new TextAreaExtension
    1.78 -  {
    1.79 -    override def paintScreenLineRange(gfx: Graphics2D,
    1.80 -      first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.81 -      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.82 -    {
    1.83 -      if (use_text_painter) {
    1.84 -        Isabelle.swing_buffer_lock(model.buffer) {
    1.85 -          val painter = text_area.getPainter
    1.86 -          val fm = painter.getFontMetrics
    1.87 -
    1.88 -          val all_chunks = line_chunks(Set[Int]() ++ physical_lines.iterator.filter(i => i != -1))
    1.89 -
    1.90 -          val x0 = text_area.getHorizontalOffset
    1.91 -          var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
    1.92 -          for (i <- 0 until physical_lines.length) {
    1.93 -            if (physical_lines(i) != -1) {
    1.94 -              all_chunks.get(start(i)) match {
    1.95 -                case Some(chunk) =>
    1.96 -                  Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR)
    1.97 -                case None =>
    1.98 -              }
    1.99 -            }
   1.100 -            y0 += line_height
   1.101 -          }
   1.102 -        }
   1.103 -      }
   1.104 -    }
   1.105 -  }
   1.106 +  val text_painter = new Text_Painter(model, text_area)
   1.107  
   1.108    private val gutter_painter = new TextAreaExtension
   1.109    {
   1.110 @@ -558,7 +481,7 @@
   1.111    {
   1.112      val painter = text_area.getPainter
   1.113      painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   1.114 -    painter.addExtension(TextAreaPainter.TEXT_LAYER + 1, text_painter)
   1.115 +    text_painter.activate()
   1.116      text_area.getGutter.addExtension(gutter_painter)
   1.117      text_area.addFocusListener(focus_listener)
   1.118      text_area.getView.addWindowListener(window_listener)
   1.119 @@ -580,7 +503,7 @@
   1.120      text_area.removeCaretListener(caret_listener)
   1.121      text_area.removeLeftOfScrollBar(overview)
   1.122      text_area.getGutter.removeExtension(gutter_painter)
   1.123 -    painter.removeExtension(text_painter)
   1.124 +    text_painter.deactivate()
   1.125      painter.removeExtension(background_painter)
   1.126      exit_popup()
   1.127    }