diff -r 364bac6691de -r 5dae03d50db1 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Jun 07 16:40:26 2021 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Jun 08 13:17:45 2021 +0200
@@ -210,6 +210,19 @@
   }
 
 
+  /* 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 */
 
   object Export