# HG changeset patch
# User immler@in.tum.de
# Date 1237546641 -3600
# Node ID 50ae42f01d451f5be9fa5b2c8c96cb552a3161ca
# Parent  5d88e0681d443909a7ae348c9c2dc30f27381a19
fixes

diff -r 5d88e0681d44 -r 50ae42f01d45 src/Tools/jEdit/src/prover/Prover.scala
--- 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)