--- a/src/Pure/PIDE/isar_document.scala Thu Sep 23 14:26:55 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala Thu Sep 23 14:39:29 2010 +0200
@@ -72,7 +72,14 @@
/* specific messages */
- def is_tracing(msg: XML.Tree): Boolean =
+ def is_ready(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.STATUS, _),
+ List(XML.Elem(Markup(Markup.READY, _), _))) => true
+ case _ => false
+ }
+
+ def is_tracing(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Markup.TRACING, _), _) => true
case _ => false