more precise notion of bad messages;
authorwenzelm
Tue, 05 Jan 2010 18:29:21 +0100
changeset 34839 3457436a1110
parent 34838 08a72dc4868e
child 34840 6c5560d48561
more precise notion of bad messages;
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)
     }