# HG changeset patch
# User wenzelm
# Date 1598624059 -7200
# Node ID d36c109bc7738c43602406c6ebc0e153f260cec8
# Parent  3afe53e8b2bab0ff7884429f48e7ba2d4b29d7cf
more robust interpretation of data;

diff -r 3afe53e8b2ba -r d36c109bc773 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Fri Aug 28 12:04:53 2020 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Fri Aug 28 16:14:19 2020 +0200
@@ -198,11 +198,12 @@
 
   val empty: ML_Statistics = apply(Nil)
 
-  def apply(ml_statistics: List[Properties.T], heading: String = "",
+  def apply(ml_statistics0: List[Properties.T], heading: String = "",
     domain: String => Boolean = (key: String) => true): ML_Statistics =
   {
-    require(ml_statistics.forall(props => Now.unapply(props).isDefined))
+    require(ml_statistics0.forall(props => Now.unapply(props).isDefined))
 
+    val ml_statistics = ml_statistics0.sortBy(now)
     val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)
     val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start
 
@@ -219,7 +220,6 @@
       val result = new mutable.ListBuffer[ML_Statistics.Entry]
       for (props <- ml_statistics) {
         val time = now(props) - time_start
-        require(time >= 0.0)
 
         // rising edges -- relative speed
         val speeds =