src/Pure/PIDE/protocol.scala

       if (is_warning(elem) || is_legacy(elem)) Output.warning_prefix(body)
       else if (is_error(elem)) Output.error_prefix(body)
       else body
 
     text1 + text2
+  }
+
+
+  /* ML profiling */
+
+  object ML_Profiling
+  {
+    def unapply(msg: XML.Tree): Option[isabelle.ML_Profiling.Report] =
+      msg match {
+        case XML.Elem(_, List(tree)) if is_warning(msg) =>
+          Markup.ML_Profiling.unapply_report(tree)
+        case _ => None
+      }
   }
 
 
   /* export */