# HG changeset patch
# User wenzelm
# Date 1314440544 -7200
# Node ID ba8f24f7156e17c4af497abf02f04ab77d640310
# Parent  3f5fd36352815bff76260d619a86ec159157dac2
de-assigned commands also count as changed;

diff -r 3f5fd3635281 -r ba8f24f7156e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Aug 27 11:22:21 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Aug 27 12:22:24 2011 +0200
@@ -296,17 +296,22 @@
       val version = the_version(id)
       val (command_execs, last_execs) = arg
 
-      val (commands, new_execs) =
+      val (changed_commands, new_execs) =
         ((Nil: List[Command], execs) /: command_execs) {
-          case ((commands1, execs1), (cmd_id, Some(exec_id))) =>
+          case ((commands1, execs1), (cmd_id, exec)) =>
             val st = the_command(cmd_id)
-            (st.command :: commands1, execs1 + (exec_id -> st))
-          case (res, (_, None)) => res
+            val commands2 = st.command :: commands1
+            val execs2 =
+              exec match {
+                case None => execs1
+                case Some(exec_id) => execs1 + (exec_id -> st)
+              }
+            (commands2, execs2)
         }
       val new_assignment = the_assignment(version).assign(command_execs, last_execs)
       val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
 
-      (commands, new_state)
+      (changed_commands, new_state)
     }
 
     def is_assigned(version: Version): Boolean =