src/Pure/PIDE/document.scala
changeset 56295 a40e67ce4f84
parent 56176 0bc9b0ad6287
child 56298 cf7710540f39
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Mar 26 14:41:52 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Mar 26 19:42:16 2014 +0100
     1.3 @@ -521,15 +521,19 @@
     1.4      def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
     1.5      def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
     1.6  
     1.7 +    def valid_id(st: Command.State)(id: Document_ID.Generic): Boolean =
     1.8 +      id == st.command.id ||
     1.9 +      (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
    1.10 +
    1.11      def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
    1.12        execs.get(id) match {
    1.13          case Some(st) =>
    1.14 -          val new_st = st + (id, message)
    1.15 +          val new_st = st + (valid_id(st), message)
    1.16            (new_st, copy(execs = execs + (id -> new_st)))
    1.17          case None =>
    1.18            commands.get(id) match {
    1.19              case Some(st) =>
    1.20 -              val new_st = st + (id, message)
    1.21 +              val new_st = st + (valid_id(st), message)
    1.22                (new_st, copy(commands = commands + (id -> new_st)))
    1.23              case None => fail
    1.24            }