tuned;

--- a/src/Pure/PIDE/session.scala	Fri Apr 03 11:29:44 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Apr 03 11:37:00 2020 +0200
@@ -493,6 +493,12 @@
               case Protocol.Theory_Timing(_, _) =>
                 theory_timings.post(Session.Theory_Timing(msg.properties.tail))
 
+              case Markup.ML_Statistics(props) =>
+                runtime_statistics.post(Session.Runtime_Statistics(props))
+
+              case Markup.Task_Statistics(props) =>
+                task_statistics.post(Session.Task_Statistics(props))
+
               case Protocol.Export(args)
               if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
                 val id = Value.Long.unapply(args.id.get).get
@@ -532,12 +538,6 @@
                   case _ => bad_output()
                 }
 
-              case Markup.ML_Statistics(props) =>
-                runtime_statistics.post(Session.Runtime_Statistics(props))
-
-              case Markup.Task_Statistics(props) =>
-                task_statistics.post(Session.Task_Statistics(props))
-
               case _ => bad_output()
             }
           }