Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/ML/ml_statistics.scala
changeset 73120 c3589f2dff31
parent 73031 f93f0597f4fb
child 73340 0ffcad1f6130 
--- a/src/Pure/ML/ml_statistics.scala	Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Sun Jan 10 13:04:29 2021 +0100
@@ -201,7 +201,7 @@
   def apply(ml_statistics0: List[Properties.T], heading: String = "",
     domain: String => Boolean = (key: String) => true): ML_Statistics =
   {
-    require(ml_statistics0.forall(props => Now.unapply(props).isDefined))
+    require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field")
 
     val ml_statistics = ml_statistics0.sortBy(now)
     val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)
isabelle