src/Pure/PIDE/document.scala
changeset 44543 ba8f24f7156e
parent 44484 470f2ee5950e
child 44580 3bc9a215a56d
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Aug 27 11:22:21 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 27 12:22:24 2011 +0200
     1.3 @@ -296,17 +296,22 @@
     1.4        val version = the_version(id)
     1.5        val (command_execs, last_execs) = arg
     1.6  
     1.7 -      val (commands, new_execs) =
     1.8 +      val (changed_commands, new_execs) =
     1.9          ((Nil: List[Command], execs) /: command_execs) {
    1.10 -          case ((commands1, execs1), (cmd_id, Some(exec_id))) =>
    1.11 +          case ((commands1, execs1), (cmd_id, exec)) =>
    1.12              val st = the_command(cmd_id)
    1.13 -            (st.command :: commands1, execs1 + (exec_id -> st))
    1.14 -          case (res, (_, None)) => res
    1.15 +            val commands2 = st.command :: commands1
    1.16 +            val execs2 =
    1.17 +              exec match {
    1.18 +                case None => execs1
    1.19 +                case Some(exec_id) => execs1 + (exec_id -> st)
    1.20 +              }
    1.21 +            (commands2, execs2)
    1.22          }
    1.23        val new_assignment = the_assignment(version).assign(command_execs, last_execs)
    1.24        val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
    1.25  
    1.26 -      (commands, new_state)
    1.27 +      (changed_commands, new_state)
    1.28      }
    1.29  
    1.30      def is_assigned(version: Version): Boolean =