diff -r 9e668ae81f97 -r 3e072441c96a src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Mar 22 16:20:53 2018 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Mar 22 16:39:22 2018 +0100
@@ -239,6 +239,13 @@
       case _ => false
     }
 
+  def is_writeln(msg: XML.Tree): Boolean =
+    msg match {
+      case XML.Elem(Markup(Markup.WRITELN, _), _) => true
+      case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true
+      case _ => false
+    }
+
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WARNING, _), _) => true
@@ -263,6 +270,9 @@
   def is_inlined(msg: XML.Tree): Boolean =
     !(is_result(msg) || is_tracing(msg) || is_state(msg))
 
+  def is_exported(msg: XML.Tree): Boolean =
+    is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
+
 
   /* breakpoints */