# HG changeset patch
# User wenzelm
# Date 1585906620 -7200
# Node ID d3abcf2360fb8079dfa7b1fe84b9fcefc93c77d9
# Parent  c87e0d81594d5d9e25eb1b0e1d07219630f6b217
tuned;

diff -r c87e0d81594d -r d3abcf2360fb src/Pure/PIDE/session.scala
--- 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()
             }
           }