--- a/src/Tools/jEdit/src/prover/Prover.scala Thu Mar 19 16:48:29 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Fri Mar 20 11:57:21 2009 +0100
@@ -145,7 +145,7 @@
// document edits
case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
- if document_versions.contains(doc_id) =>
+ if document_versions.exists(dv => doc_id == dv._1) =>
output_info.event(result.toString)
for {
XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
@@ -154,7 +154,7 @@
if (commands.contains(cmd_id)) {
val cmd = commands(cmd_id)
if (cmd.state_id != null) states -= cmd.state_id
- states(cmd_id) = cmd
+ states(state_id) = cmd
cmd.state_id = state_id
cmd.status = Command.Status.UNPROCESSED
command_change(cmd)