src/Pure/Admin/build_status.scala
changeset 65863 94fe5e82d101
parent 65861 f35abc25d7b1
child 65865 177b90f33f40
     1.1 --- a/src/Pure/Admin/build_status.scala	Thu May 18 11:17:53 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Thu May 18 11:42:16 2017 +0200
     1.3 @@ -70,17 +70,8 @@
     1.4    {
     1.5      require(entries.nonEmpty)
     1.6  
     1.7 -    def pull_date: Date = entries.head.pull_date
     1.8 -    def isabelle_version: String = entries.head.isabelle_version
     1.9 -    def afp_version: String = entries.head.afp_version
    1.10 -
    1.11 -    def timing: Timing = entries.head.timing
    1.12 -    def ml_timing: Timing = entries.head.ml_timing
    1.13 -    def order: Long = - timing.elapsed.ms
    1.14 -
    1.15 -    def maximum_heap: Long = entries.head.maximum_heap
    1.16 -    def average_heap: Long = entries.head.average_heap
    1.17 -    def final_heap: Long = entries.head.final_heap
    1.18 +    def head: Entry = entries.head
    1.19 +    def order: Long = - head.timing.elapsed.ms
    1.20  
    1.21      def check_timing: Boolean = entries.length >= 3
    1.22      def check_heap: Boolean =
    1.23 @@ -363,24 +354,24 @@
    1.24            List(HTML.itemize(
    1.25              data_entry.sessions.map(session =>
    1.26                HTML.link("#session_" + session.name, HTML.text(session.name)) ::
    1.27 -              HTML.text(" (" + session.timing.message_resources + ")"))))) ::
    1.28 +              HTML.text(" (" + session.head.timing.message_resources + ")"))))) ::
    1.29          data_entry.sessions.flatMap(session =>
    1.30            List(
    1.31              HTML.section(session.name) + HTML.id("session_" + session.name),
    1.32              HTML.par(
    1.33                HTML.description(
    1.34                  List(
    1.35 -                  HTML.text("timing:") -> HTML.text(session.timing.message_resources),
    1.36 -                  HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) :::
    1.37 -                print_heap(session.maximum_heap).map(s =>
    1.38 +                  HTML.text("timing:") -> HTML.text(session.head.timing.message_resources),
    1.39 +                  HTML.text("ML timing:") -> HTML.text(session.head.ml_timing.message_resources)) :::
    1.40 +                print_heap(session.head.maximum_heap).map(s =>
    1.41                    HTML.text("maximum heap:") -> HTML.text(s)).toList :::
    1.42 -                print_heap(session.average_heap).map(s =>
    1.43 +                print_heap(session.head.average_heap).map(s =>
    1.44                    HTML.text("average heap:") -> HTML.text(s)).toList :::
    1.45 -                print_heap(session.final_heap).map(s =>
    1.46 +                print_heap(session.head.final_heap).map(s =>
    1.47                    HTML.text("final heap:") -> HTML.text(s)).toList :::
    1.48 -                proper_string(session.isabelle_version).map(s =>
    1.49 +                proper_string(session.head.isabelle_version).map(s =>
    1.50                    HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
    1.51 -                proper_string(session.afp_version).map(s =>
    1.52 +                proper_string(session.head.afp_version).map(s =>
    1.53                    HTML.text("AFP version:") -> HTML.text(s)).toList) ::
    1.54                session_plots.getOrElse(session.name, Nil).map(plot_name =>
    1.55                  HTML.image(plot_name) +