diff -r 20bba9cc4b51 -r 53365ba766ac src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Wed Sep 22 22:25:21 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Wed Sep 22 22:39:17 2010 +0200
@@ -72,6 +72,12 @@
 
   /* specific messages */
 
+  def is_tracing(msg: XML.Tree): Boolean =
+    msg match {
+      case XML.Elem(Markup(Markup.TRACING, _), _) => true
+      case _ => false
+    }
+
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WARNING, _), _) => true