src/Tools/jEdit/src/document_view.scala
changeset 43419 6ed49c52d463
parent 43417 83be997a11d6
child 43448 90aec5043461
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Jun 17 00:10:39 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Jun 17 13:55:53 2011 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4    private val session = model.session
     1.5  
     1.6  
     1.7 -  /** robust extension body **/
     1.8 +  /* robust extension body */
     1.9  
    1.10    def robust_body[A](default: A)(body: => A): A =
    1.11    {
    1.12 @@ -85,8 +85,6 @@
    1.13    }
    1.14  
    1.15  
    1.16 -  /** token handling **/
    1.17 -
    1.18    /* visible line ranges */
    1.19  
    1.20    // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
    1.21 @@ -112,6 +110,31 @@
    1.22    }
    1.23  
    1.24  
    1.25 +  /* snapshot */
    1.26 +
    1.27 +  // owned by Swing thread
    1.28 +  @volatile private var was_outdated = false
    1.29 +  @volatile private var was_updated = false
    1.30 +
    1.31 +  def update_snapshot(): Document.Snapshot =
    1.32 +  {
    1.33 +    Swing_Thread.require()
    1.34 +    val snapshot = model.snapshot()
    1.35 +    was_updated = was_outdated && !snapshot.is_outdated
    1.36 +    was_outdated = was_outdated || snapshot.is_outdated
    1.37 +    snapshot
    1.38 +  }
    1.39 +
    1.40 +  def flush_snapshot(): (Boolean, Document.Snapshot) =
    1.41 +  {
    1.42 +    Swing_Thread.require()
    1.43 +    val snapshot = update_snapshot()
    1.44 +    val updated = was_updated
    1.45 +    if (updated) { was_outdated = false; was_updated = false }
    1.46 +    (updated, snapshot)
    1.47 +  }
    1.48 +
    1.49 +
    1.50    /* HTML popups */
    1.51  
    1.52    private var html_popup: Option[Popup] = None
    1.53 @@ -196,7 +219,7 @@
    1.54        if (!model.buffer.isLoaded) exit_control()
    1.55        else
    1.56          Isabelle.swing_buffer_lock(model.buffer) {
    1.57 -          val snapshot = model.snapshot
    1.58 +          val snapshot = update_snapshot()
    1.59  
    1.60            if (control) init_popup(snapshot, x, y)
    1.61  
    1.62 @@ -217,7 +240,7 @@
    1.63      override def getToolTipText(x: Int, y: Int): String =
    1.64      {
    1.65        robust_body(null: String) {
    1.66 -        val snapshot = model.snapshot()
    1.67 +        val snapshot = update_snapshot()
    1.68          val offset = text_area.xyToOffset(x, y)
    1.69          if (control) {
    1.70            snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
    1.71 @@ -249,14 +272,14 @@
    1.72          val width = GutterOptionPane.getSelectionAreaWidth
    1.73          val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
    1.74          val FOLD_MARKER_SIZE = 12
    1.75 -  
    1.76 +
    1.77          if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
    1.78            Isabelle.swing_buffer_lock(model.buffer) {
    1.79 -            val snapshot = model.snapshot()
    1.80 +            val snapshot = update_snapshot()
    1.81              for (i <- 0 until physical_lines.length) {
    1.82                if (physical_lines(i) != -1) {
    1.83                  val line_range = proper_line_range(start(i), end(i))
    1.84 -  
    1.85 +
    1.86                  // gutter icons
    1.87                  val icons =
    1.88                    (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
    1.89 @@ -284,7 +307,7 @@
    1.90    def selected_command(): Option[Command] =
    1.91    {
    1.92      Swing_Thread.require()
    1.93 -    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
    1.94 +    update_snapshot().node.proper_command_at(text_area.getCaretPosition)
    1.95    }
    1.96  
    1.97    private val caret_listener = new CaretListener {
    1.98 @@ -331,7 +354,7 @@
    1.99  
   1.100        val buffer = model.buffer
   1.101        Isabelle.buffer_lock(buffer) {
   1.102 -        val snapshot = model.snapshot()
   1.103 +        val snapshot = update_snapshot()
   1.104  
   1.105          def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] =
   1.106          {
   1.107 @@ -372,22 +395,26 @@
   1.108          case Session.Commands_Changed(changed) =>
   1.109            val buffer = model.buffer
   1.110            Isabelle.swing_buffer_lock(buffer) {
   1.111 -            val snapshot = model.snapshot()
   1.112 +            val (updated, snapshot) = flush_snapshot()
   1.113 +            val visible_range = screen_lines_range()
   1.114  
   1.115 -            if (changed.exists(snapshot.node.commands.contains))
   1.116 +            if (updated || changed.exists(snapshot.node.commands.contains))
   1.117                overview.repaint()
   1.118  
   1.119 -            val visible_range = screen_lines_range()
   1.120 -            val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
   1.121 -            if (visible_cmds.exists(changed)) {
   1.122 -              for {
   1.123 -                line <- 0 until text_area.getVisibleLines
   1.124 -                val start = text_area.getScreenLineStartOffset(line) if start >= 0
   1.125 -                val end = text_area.getScreenLineEndOffset(line) if end >= 0
   1.126 -                val range = proper_line_range(start, end)
   1.127 -                val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
   1.128 -                if line_cmds.exists(changed)
   1.129 -              } text_area.invalidateScreenLineRange(line, line)
   1.130 +            if (updated) invalidate_line_range(visible_range)
   1.131 +            else {
   1.132 +              val visible_cmds =
   1.133 +                snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
   1.134 +              if (visible_cmds.exists(changed)) {
   1.135 +                for {
   1.136 +                  line <- 0 until text_area.getVisibleLines
   1.137 +                  val start = text_area.getScreenLineStartOffset(line) if start >= 0
   1.138 +                  val end = text_area.getScreenLineEndOffset(line) if end >= 0
   1.139 +                  val range = proper_line_range(start, end)
   1.140 +                  val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
   1.141 +                  if line_cmds.exists(changed)
   1.142 +                } text_area.invalidateScreenLineRange(line, line)
   1.143 +              }
   1.144              }
   1.145            }
   1.146