flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);

--- a/src/Tools/jEdit/src/document_view.scala	Fri Jun 17 00:10:39 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Fri Jun 17 13:55:53 2011 +0200
@@ -69,7 +69,7 @@
   private val session = model.session
 
 
-  /** robust extension body **/
+  /* robust extension body */
 
   def robust_body[A](default: A)(body: => A): A =
   {
@@ -85,8 +85,6 @@
   }
 
 
-  /** token handling **/
-
   /* visible line ranges */
 
   // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
@@ -112,6 +110,31 @@
   }
 
 
+  /* snapshot */
+
+  // owned by Swing thread
+  @volatile private var was_outdated = false
+  @volatile private var was_updated = false
+
+  def update_snapshot(): Document.Snapshot =
+  {
+    Swing_Thread.require()
+    val snapshot = model.snapshot()
+    was_updated = was_outdated && !snapshot.is_outdated
+    was_outdated = was_outdated || snapshot.is_outdated
+    snapshot
+  }
+
+  def flush_snapshot(): (Boolean, Document.Snapshot) =
+  {
+    Swing_Thread.require()
+    val snapshot = update_snapshot()
+    val updated = was_updated
+    if (updated) { was_outdated = false; was_updated = false }
+    (updated, snapshot)
+  }
+
+
   /* HTML popups */
 
   private var html_popup: Option[Popup] = None
@@ -196,7 +219,7 @@
       if (!model.buffer.isLoaded) exit_control()
       else
         Isabelle.swing_buffer_lock(model.buffer) {
-          val snapshot = model.snapshot
+          val snapshot = update_snapshot()
 
           if (control) init_popup(snapshot, x, y)
 
@@ -217,7 +240,7 @@
     override def getToolTipText(x: Int, y: Int): String =
     {
       robust_body(null: String) {
-        val snapshot = model.snapshot()
+        val snapshot = update_snapshot()
         val offset = text_area.xyToOffset(x, y)
         if (control) {
           snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
@@ -249,14 +272,14 @@
         val width = GutterOptionPane.getSelectionAreaWidth
         val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
         val FOLD_MARKER_SIZE = 12
-  
+
         if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
           Isabelle.swing_buffer_lock(model.buffer) {
-            val snapshot = model.snapshot()
+            val snapshot = update_snapshot()
             for (i <- 0 until physical_lines.length) {
               if (physical_lines(i) != -1) {
                 val line_range = proper_line_range(start(i), end(i))
-  
+
                 // gutter icons
                 val icons =
                   (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
@@ -284,7 +307,7 @@
   def selected_command(): Option[Command] =
   {
     Swing_Thread.require()
-    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
+    update_snapshot().node.proper_command_at(text_area.getCaretPosition)
   }
 
   private val caret_listener = new CaretListener {
@@ -331,7 +354,7 @@
 
       val buffer = model.buffer
       Isabelle.buffer_lock(buffer) {
-        val snapshot = model.snapshot()
+        val snapshot = update_snapshot()
 
         def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] =
         {
@@ -372,22 +395,26 @@
         case Session.Commands_Changed(changed) =>
           val buffer = model.buffer
           Isabelle.swing_buffer_lock(buffer) {
-            val snapshot = model.snapshot()
+            val (updated, snapshot) = flush_snapshot()
+            val visible_range = screen_lines_range()
 
-            if (changed.exists(snapshot.node.commands.contains))
+            if (updated || changed.exists(snapshot.node.commands.contains))
               overview.repaint()
 
-            val visible_range = screen_lines_range()
-            val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
-            if (visible_cmds.exists(changed)) {
-              for {
-                line <- 0 until text_area.getVisibleLines
-                val start = text_area.getScreenLineStartOffset(line) if start >= 0
-                val end = text_area.getScreenLineEndOffset(line) if end >= 0
-                val range = proper_line_range(start, end)
-                val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
-                if line_cmds.exists(changed)
-              } text_area.invalidateScreenLineRange(line, line)
+            if (updated) invalidate_line_range(visible_range)
+            else {
+              val visible_cmds =
+                snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
+              if (visible_cmds.exists(changed)) {
+                for {
+                  line <- 0 until text_area.getVisibleLines
+                  val start = text_area.getScreenLineStartOffset(line) if start >= 0
+                  val end = text_area.getScreenLineEndOffset(line) if end >= 0
+                  val range = proper_line_range(start, end)
+                  val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
+                  if line_cmds.exists(changed)
+                } text_area.invalidateScreenLineRange(line, line)
+              }
             }
           }
 

--- a/src/Tools/jEdit/src/output_dockable.scala	Fri Jun 17 00:10:39 2011 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Jun 17 13:55:53 2011 +0200
@@ -34,7 +34,7 @@
         Document_View(view.getTextArea) match {
           case Some(doc_view) =>
             val cmd = current_command.get
-            val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get
+            val start_ofs = doc_view.update_snapshot().node.command_start(cmd).get
             val buffer = view.getBuffer
             buffer.beginCompoundEdit()
             buffer.remove(start_ofs, cmd.length)
@@ -83,7 +83,7 @@
         case Some(doc_view) =>
           current_command match {
             case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
-              val snapshot = doc_view.model.snapshot()
+              val snapshot = doc_view.update_snapshot()
               val filtered_results =
                 snapshot.state(cmd).results.iterator.map(_._2) filter {
                   case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing  // FIXME not scalable

--- a/src/Tools/jEdit/src/text_area_painter.scala	Fri Jun 17 00:10:39 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Fri Jun 17 13:55:53 2011 +0200
@@ -53,7 +53,7 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       doc_view.robust_body(()) {
-        painter_snapshot = model.snapshot()
+        painter_snapshot = doc_view.update_snapshot()
         painter_clip = gfx.getClip
       }
     }