# HG changeset patch
# User wenzelm
# Date 1253113994 -7200
# Node ID ec35626a2aa58a765a583bee2db96a1c8bde9bb3
# Parent  34b0aadab7ee7dc50508c9e7e94fb0178e8a6899
misc tuning;

diff -r 34b0aadab7ee -r ec35626a2aa5 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Wed Sep 16 00:14:01 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Wed Sep 16 17:13:14 2009 +0200
@@ -65,13 +65,13 @@
   @volatile private var states = Map[Isar_Document.State_ID, Command_State]()
   @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
   val document_0 =
-  ProofDocument.empty.
-  set_command_keyword((s: String) => command_decls().contains(s))
+    ProofDocument.empty.
+    set_command_keyword((s: String) => command_decls().contains(s))
   @volatile private var document_versions = List(document_0)
 
   def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
   def document(id: Isar_Document.Document_ID): Option[ProofDocument] =
-  document_versions.find(_.id == id)
+    document_versions.find(_.id == id)
 
 
   /* prover results */
@@ -86,13 +86,10 @@
     val message = Isabelle_Process.parse_message(system, result)
 
     val state =
-    result.props.find(p => p._1 == Markup.ID) match {
-      case None => None
-      case Some((_, id)) =>
-        if (commands.contains(id)) Some(commands(id))
-        else if (states.contains(id)) Some(states(id))
-        else None
-    }
+      Position.id_of(result.props) match {
+        case None => None
+        case Some(id) => commands.get(id) orElse states.get(id) orElse None
+      }
     if (state.isDefined) state.get ! (this, message)
     else if (result.kind == Isabelle_Process.Kind.STATUS) {
       //{{{ global status message
@@ -101,25 +98,26 @@
           for (elem <- elems) {
             elem match {
               // document edits
-              case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
-                if document_versions.exists(_.id == doc_id) =>
-                val doc = document_versions.find(_.id == doc_id).get
-                for {
-                  XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
-                  <- edits
-                } {
-                  if (commands.contains(cmd_id)) {
-                    val cmd = commands(cmd_id)
-                    val state = new Command_State(cmd)
-                    states += (state_id -> state)
-                    doc.states += (cmd -> state)
-                    command_change.event(cmd)
-                  }
+              case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) =>
+                document_versions.find(_.id == doc_id) match {
+                  case Some(doc) =>
+                    for {
+                      XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
+                      <- edits
+                    } {
+                      if (commands.contains(cmd_id)) {
+                        val cmd = commands(cmd_id)
+                        val state = new Command_State(cmd)
+                        states += (state_id -> state)
+                        doc.states += (cmd -> state)
+                        command_change.event(cmd)
+                     }
+                    }
+                  case None =>
                 }
 
                 // command and keyword declarations
-              case XML.Elem(Markup.COMMAND_DECL,
-                            (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
+              case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
                 _command_decls += (name -> kind)
                 _completion += name
               case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>