--- a/src/Pure/PIDE/document.scala Mon Aug 30 11:35:17 2010 +0200
+++ b/src/Pure/PIDE/document.scala Mon Aug 30 13:01:32 2010 +0200
@@ -204,7 +204,7 @@
def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
- def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
+ def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
execs.get(id) match {
case Some((st, occs)) =>
val new_st = st.accumulate(message)