src/Pure/Admin/build_status.scala
changeset 65866 00e8b836d4db
parent 65865 177b90f33f40
child 65867 53613acb76e7
     1.1 --- a/src/Pure/Admin/build_status.scala	Thu May 18 14:14:20 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Thu May 18 14:38:09 2017 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4        entries.forall(entry =>
     1.5          entry.maximum_heap > 0 ||
     1.6          entry.average_heap > 0 ||
     1.7 -        entry.final_heap > 0)
     1.8 +        entry.stored_heap > 0)
     1.9    }
    1.10    sealed case class Entry(
    1.11      pull_date: Date,
    1.12 @@ -90,7 +90,7 @@
    1.13      ml_timing: Timing,
    1.14      maximum_heap: Long,
    1.15      average_heap: Long,
    1.16 -    final_heap: Long)
    1.17 +    stored_heap: Long)
    1.18  
    1.19    sealed case class Image(name: String, width: Int, height: Int)
    1.20    {
    1.21 @@ -174,7 +174,7 @@
    1.22                ML_Statistics(
    1.23                  if (ml_statistics)
    1.24                    Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics))
    1.25 -                else Nil, heading = session_name + " (Isabelle/ " + isabelle_version + ")")
    1.26 +                else Nil, heading = session_name + " (Isabelle/" + isabelle_version + ")")
    1.27  
    1.28              val entry =
    1.29                Entry(
    1.30 @@ -193,7 +193,7 @@
    1.31                      Build_Log.Data.ml_timing_gc),
    1.32                  maximum_heap = ml_stats.maximum_heap_size,
    1.33                  average_heap = ml_stats.average_heap_size,
    1.34 -                final_heap = res.long(Build_Log.Data.heap_size))
    1.35 +                stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)))
    1.36  
    1.37              val sessions = data_entries.getOrElse(data_name, Map.empty)
    1.38              val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
    1.39 @@ -229,13 +229,8 @@
    1.40      def clean_name(name: String): String =
    1.41        name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
    1.42  
    1.43 -    def heap_scale(x: Long): Long = x / 1024 / 1024
    1.44 -
    1.45      def print_heap(x: Long): Option[String] =
    1.46 -    {
    1.47 -      val y = heap_scale(x)
    1.48 -      if (y == 0L) None else Some(y.toString + " M")
    1.49 -    }
    1.50 +      if (x == 0L) None else Some(x.toString + " M")
    1.51  
    1.52      HTML.write_document(target_dir, "index.html",
    1.53        List(HTML.title("Isabelle build status")),
    1.54 @@ -274,9 +269,9 @@
    1.55                        entry.timing.resources.minutes,
    1.56                        entry.ml_timing.elapsed.minutes,
    1.57                        entry.ml_timing.resources.minutes,
    1.58 -                      heap_scale(entry.maximum_heap),
    1.59 -                      heap_scale(entry.average_heap),
    1.60 -                      heap_scale(entry.final_heap)).mkString(" "))))
    1.61 +                      entry.maximum_heap,
    1.62 +                      entry.average_heap,
    1.63 +                      entry.stored_heap).mkString(" "))))
    1.64  
    1.65                val max_time =
    1.66                  ((0.0 /: session.entries){ case (m, entry) =>
    1.67 @@ -394,8 +389,8 @@
    1.68                    HTML.text("maximum heap:") -> HTML.text(s)).toList :::
    1.69                  print_heap(session.head.average_heap).map(s =>
    1.70                    HTML.text("average heap:") -> HTML.text(s)).toList :::
    1.71 -                print_heap(session.head.final_heap).map(s =>
    1.72 -                  HTML.text("final heap:") -> HTML.text(s)).toList :::
    1.73 +                print_heap(session.head.stored_heap).map(s =>
    1.74 +                  HTML.text("stored heap:") -> HTML.text(s)).toList :::
    1.75                  proper_string(session.head.isabelle_version).map(s =>
    1.76                    HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
    1.77                  proper_string(session.head.afp_version).map(s =>