Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned output;
authorwenzelm
Thu, 13 Jul 2023 13:51:08 +0200
changeset 78330 1a69d3a3e3aa
parent 78329 a041d49736f2
child 78331 cefe819c5980
tuned output;
src/Pure/Tools/profiling.scala file | annotate | diff | comparison | revisions 
--- a/src/Pure/Tools/profiling.scala	Thu Jul 13 13:10:40 2023 +0200
+++ b/src/Pure/Tools/profiling.scala	Thu Jul 13 13:51:08 2023 +0200
@@ -119,7 +119,8 @@
         "types_size%",
         "spaces_size%")
 
-    def header: List[String] = "session" :: header0 ::: header0.map(_ + "_cumulative")
+    def header: List[String] =
+      "session" :: header0.flatMap(a => List(a, "\u2211" + a))
   }
 
   final class Statistics private(
@@ -142,7 +143,7 @@
     private def thms_percentage(thms: Int): Percentage =
       percentage(thms, locale_thms + global_thms)
 
-    def fields0: List[Any] =
+    val fields0: List[Any] =
       List(
         theories,
         locales,
@@ -157,7 +158,8 @@
         size_percentage(types_size).toString,
         size_percentage(spaces_size).toString)
 
-    def fields: List[Any] = session :: fields0 ::: cumulative.fields0
+    def fields: List[Any] =
+      session :: fields0.zipWithIndex.flatMap({ case (a, i) => List(a, cumulative.fields0(i)) })
 
     lazy val cumulative: Statistics =
       parent match {
isabelle