--- 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()
}
}