# HG changeset patch
# User wenzelm
# Date 1262712561 -3600
# Node ID 3457436a1110f89a54cf0d6efa044b9b090d58ab
# Parent  08a72dc4868e1106ee2e6a1bb2ba7c2a492d45f2
more precise notion of bad messages;

diff -r 08a72dc4868e -r 3457436a1110 src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Tue Jan 05 18:23:39 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Tue Jan 05 18:29:21 2010 +0100
@@ -146,12 +146,12 @@
           case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) =>
             syntax += name
 
-          case _ => bad_result(result)
+          case _ => if (!result.is_ready) bad_result(result)
         }
       }
       else if (result.kind == Isabelle_Process.Kind.EXIT)
         prover = null
-      else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_ready)
+      else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_raw)
         bad_result(result)
     }