more output;
authorwenzelm
Wed May 17 23:05:30 2017 +0200 (2017-05-17)
changeset 65860ce6be2e40d47
parent 65859 95ddb6dea0d5
child 65861 f35abc25d7b1
more output;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Wed May 17 22:32:48 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Wed May 17 23:05:30 2017 +0200
     1.3 @@ -78,6 +78,10 @@
     1.4      def ml_timing: Timing = entries.head.ml_timing
     1.5      def order: Long = - timing.elapsed.ms
     1.6  
     1.7 +    def maximum_heap: Long = entries.head.maximum_heap
     1.8 +    def average_heap: Long = entries.head.average_heap
     1.9 +    def final_heap: Long = entries.head.final_heap
    1.10 +
    1.11      def check_timing: Boolean = entries.length >= 3
    1.12      def check_heap: Boolean =
    1.13        entries.length >= 3 &&
    1.14 @@ -230,7 +234,13 @@
    1.15      def clean_name(name: String): String =
    1.16        name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
    1.17  
    1.18 -    def heap_scale(x: Long): Double = x.toDouble / (1024 * 1024)
    1.19 +    def heap_scale(x: Long): Long = x / 1024 / 1024
    1.20 +
    1.21 +    def print_heap(x: Long): Option[String] =
    1.22 +    {
    1.23 +      val y = heap_scale(x)
    1.24 +      if (y == 0L) None else Some(y.toString + " M")
    1.25 +    }
    1.26  
    1.27      HTML.write_document(target_dir, "index.html",
    1.28        List(HTML.title("Isabelle build status")),
    1.29 @@ -364,6 +374,12 @@
    1.30                  List(
    1.31                    HTML.text("timing:") -> HTML.text(session.timing.message_resources),
    1.32                    HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) :::
    1.33 +                print_heap(session.maximum_heap).map(s =>
    1.34 +                  HTML.text("maximum heap:") -> HTML.text(s)).toList :::
    1.35 +                print_heap(session.average_heap).map(s =>
    1.36 +                  HTML.text("average heap:") -> HTML.text(s)).toList :::
    1.37 +                print_heap(session.final_heap).map(s =>
    1.38 +                  HTML.text("final heap:") -> HTML.text(s)).toList :::
    1.39                  proper_string(session.isabelle_version).map(s =>
    1.40                    HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
    1.41                  proper_string(session.afp_version).map(s =>