# HG changeset patch
# User wenzelm
# Date 1262630555 -3600
# Node ID b83c7a738eb8d18d8ae2a99f65bdc840c04f1f88
# Parent  67733fd0e3fa08078103f692e89008f5361b6fb4
singleton status messages, with more precise patterns -- report bad messages;

diff -r 67733fd0e3fa -r b83c7a738eb8 src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Mon Jan 04 19:08:10 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Mon Jan 04 19:42:35 2010 +0100
@@ -102,6 +102,11 @@
 
     /* prover results */
 
+    def bad_result(result: Isabelle_Process.Result)
+    {
+      System.err.println("Ignoring prover result: " + result)
+    }
+
     def handle_result(result: Isabelle_Process.Result)
     {
       raw_results.event(result)
@@ -115,38 +120,38 @@
       if (target.isDefined) target.get.consume(this, result.message)
       else if (result.kind == Isabelle_Process.Kind.STATUS) {
         // global status message
-        for (elem <- result.body) {
-          elem match {
-            // document state assigment
-            case XML.Elem(Markup.ASSIGN, _, edits) if target_id.isDefined =>
-              documents.get(target_id.get) match {
-                case Some(doc) =>
-                  val states =
-                    for {
-                      XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
-                        <- edits
-                      cmd <- lookup_command(cmd_id)
-                    } yield {
-                      val st = cmd.assign_state(state_id)
-                      register(st)
-                      (cmd, st)
-                    }
-                  doc.assign_states(states)
-                case None =>
-              }
+        result.body match {
 
-            // command and keyword declarations
-            case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
-              syntax += (name, kind)
-            case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
-              syntax += name
+          // document state assigment
+          case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined =>
+            documents.get(target_id.get) match {
+              case Some(doc) =>
+                val states =
+                  for {
+                    XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
+                      <- edits
+                    cmd <- lookup_command(cmd_id)
+                  } yield {
+                    val st = cmd.assign_state(state_id)
+                    register(st)
+                    (cmd, st)
+                  }
+                doc.assign_states(states)
+              case None => bad_result(result)
+            }
 
-            case _ =>
-          }
+          // command and keyword declarations
+          case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) =>
+            syntax += (name, kind)
+          case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) =>
+            syntax += name
+
+          case _ => bad_result(result)
         }
       }
       else if (result.kind == Isabelle_Process.Kind.EXIT)
         prover = null
+      else if (result.kind != Isabelle_Process.Kind.STDIN) bad_result(result)
     }