src/Pure/PIDE/document.scala
changeset 49527 b96e4a39cc3e
parent 49414 d7b5fb2e9ca2
child 49645 5a0817ec0314
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Sep 22 19:16:48 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Sep 22 19:23:04 2012 +0200
     1.3 @@ -373,12 +373,12 @@
     1.4      def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
     1.5        execs.get(id) match {
     1.6          case Some(st) =>
     1.7 -          val new_st = st + message
     1.8 +          val new_st = st + (id, message)
     1.9            (new_st, copy(execs = execs + (id -> new_st)))
    1.10          case None =>
    1.11            commands.get(id) match {
    1.12              case Some(st) =>
    1.13 -              val new_st = st + message
    1.14 +              val new_st = st + (id, message)
    1.15                (new_st, copy(commands = commands + (id -> new_st)))
    1.16              case None => fail
    1.17            }