explicit propagation of assignment event, even if changed command set is empty;
discontinued slightly odd Document_View.update_snapshot/flush_snapshot;

--- a/src/Pure/System/session.scala	Mon Mar 19 21:52:09 2012 +0100
+++ b/src/Pure/System/session.scala	Mon Mar 19 23:08:27 2012 +0100
@@ -24,7 +24,8 @@
   //{{{
   case object Global_Settings
   case object Caret_Focus
-  case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])
+  case class Commands_Changed(
+    assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
   sealed abstract class Phase
   case object Inactive extends Phase
@@ -227,9 +228,9 @@
 
     object delay_commands_changed
     {
+      private var changed_assignment: Boolean = false
       private var changed_nodes: Set[Document.Node.Name] = Set.empty
       private var changed_commands: Set[Command] = Set.empty
-      private def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
 
       private var flush_time: Option[Long] = None
 
@@ -241,17 +242,22 @@
 
       def flush()
       {
-        if (changed)
-          commands_changed_buffer ! Session.Commands_Changed(changed_nodes, changed_commands)
+        if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty)
+          commands_changed_buffer !
+            Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands)
+        changed_assignment = false
         changed_nodes = Set.empty
         changed_commands = Set.empty
         flush_time = None
       }
 
-      def invoke(command: Command)
+      def invoke(assign: Boolean, commands: List[Command])
       {
-        changed_nodes += command.node_name
-        changed_commands += command
+        changed_assignment |= assign
+        for (command <- commands) {
+          changed_nodes += command.node_name
+          changed_commands += command
+        }
         val now = System.currentTimeMillis()
         flush_time match {
           case None => flush_time = Some(now + output_delay.ms)
@@ -304,22 +310,16 @@
     /* exec state assignment */
 
     def handle_assign(id: Document.Version_ID, assign: Document.Assign)
-    //{{{
     {
       val cmds = global_state >>> (_.assign(id, assign))
-      for (cmd <- cmds) delay_commands_changed.invoke(cmd)
+      delay_commands_changed.invoke(true, cmds)
     }
-    //}}}
 
 
     /* removed versions */
 
-    def handle_removed(removed: List[Document.Version_ID])
-    //{{{
-    {
+    def handle_removed(removed: List[Document.Version_ID]): Unit =
       global_state >> (_.removed_versions(removed))
-    }
-    //}}}
 
 
     /* resulting changes */
@@ -367,7 +367,7 @@
         case Position.Id(state_id) if !output.is_protocol =>
           try {
             val st = global_state >>> (_.accumulate(state_id, output.message))
-            delay_commands_changed.invoke(st.command)
+            delay_commands_changed.invoke(false, List(st.command))
           }
           catch {
             case _: Document.State.Fail => bad_output(output)

--- a/src/Tools/jEdit/src/document_view.scala	Mon Mar 19 21:52:09 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Mar 19 23:08:27 2012 +0100
@@ -144,31 +144,6 @@
   }
 
 
-  /* 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 &&= !snapshot.is_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
@@ -242,7 +217,7 @@
       if (!model.buffer.isLoaded) exit_control()
       else
         Isabelle.buffer_lock(model.buffer) {
-          val snapshot = update_snapshot()
+          val snapshot = model.snapshot()
 
           if (control) init_popup(snapshot, x, y)
 
@@ -268,7 +243,7 @@
     override def getToolTipText(x: Int, y: Int): String =
     {
       robust_body(null: String) {
-        val snapshot = update_snapshot()
+        val snapshot = model.snapshot()
         val offset = text_area.xyToOffset(x, y)
         val range = Text.Range(offset, offset + 1)
         val tip =
@@ -295,7 +270,7 @@
 
         if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
           Isabelle.buffer_lock(model.buffer) {
-            val snapshot = update_snapshot()
+            val snapshot = model.snapshot()
             for (i <- 0 until physical_lines.length) {
               if (physical_lines(i) != -1) {
                 val line_range = proper_line_range(start(i), end(i))
@@ -340,7 +315,7 @@
   def selected_command(): Option[Command] =
   {
     Swing_Thread.require()
-    update_snapshot().node.command_at(text_area.getCaretPosition).map(_._1)
+    model.snapshot().node.command_at(text_area.getCaretPosition).map(_._1)
   }
 
   private val delay_caret_update =
@@ -372,16 +347,16 @@
           Swing_Thread.later {
             Isabelle.buffer_lock(buffer) {
               if (model.buffer == text_area.getBuffer) {
-                val (updated, snapshot) = flush_snapshot()
+                val snapshot = model.snapshot()
 
-                if (updated ||
+                if (changed.assignment ||
                     (changed.nodes.contains(model.name) &&
                      changed.commands.exists(snapshot.node.commands.contains)))
                   overview.delay_repaint(true)
 
                 visible_range() match {
                   case Some(visible) =>
-                    if (updated) invalidate_range(visible)
+                    if (changed.assignment) invalidate_range(visible)
                     else {
                       val visible_cmds =
                         snapshot.node.command_range(snapshot.revert(visible)).map(_._1)

--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Mar 19 21:52:09 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Mar 19 23:08:27 2012 +0100
@@ -35,7 +35,7 @@
         Document_View(view.getTextArea) match {
           case Some(doc_view) =>
             val cmd = current_command.get
-            val start_ofs = doc_view.update_snapshot().node.command_start(cmd).get
+            val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get
             val buffer = view.getBuffer
             buffer.beginCompoundEdit()
             buffer.remove(start_ofs, cmd.length)
@@ -84,7 +84,7 @@
         case Some(doc_view) =>
           current_command match {
             case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
-              val snapshot = doc_view.update_snapshot()
+              val snapshot = doc_view.model.snapshot()
               val filtered_results =
                 snapshot.state.command_state(snapshot.version, cmd).results.iterator
                   .map(_._2).filter(

--- a/src/Tools/jEdit/src/text_area_painter.scala	Mon Mar 19 21:52:09 2012 +0100
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Mon Mar 19 23:08:27 2012 +0100
@@ -84,7 +84,7 @@
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
-      painter_snapshot = doc_view.update_snapshot()
+      painter_snapshot = model.snapshot()
       painter_clip = gfx.getClip
     }
   }

--- a/src/Tools/jEdit/src/text_overview.scala	Mon Mar 19 21:52:09 2012 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Mon Mar 19 23:08:27 2012 +0100
@@ -55,7 +55,7 @@
 
     doc_view.robust_body(()) {
       Isabelle.buffer_lock(buffer) {
-        val snapshot = doc_view.update_snapshot()
+        val snapshot = doc_view.model.snapshot()
 
         gfx.setColor(getBackground)
         gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)