src/Tools/jEdit/src/document_view.scala
changeset 43376 0f6880c1c759
parent 43369 4c86b3405010
child 43381 806878ae2219
     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  }