tuned output;
authorwenzelm
Sat Feb 23 21:48:18 2019 +0100 (7 weeks ago ago)
changeset 70014c3500cec8290
parent 70013 b614e3e4146a
child 70015 58ef3b8a8460
tuned output;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat Feb 23 21:33:09 2019 +0100
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sat Feb 23 21:48:18 2019 +0100
     1.3 @@ -483,12 +483,12 @@
     1.4  
     1.5                val heap_plots =
     1.6                  List(
     1.7 -                  """ using 1:6 smooth sbezier title "maximum heap (smooth)" """,
     1.8 -                  """ using 1:6 smooth csplines title "maximum heap" """,
     1.9 -                  """ using 1:7 smooth sbezier title "average heap (smooth)" """,
    1.10 -                  """ using 1:7 smooth csplines title "average heap" """,
    1.11 -                  """ using 1:8 smooth sbezier title "stored heap (smooth)" """,
    1.12 -                  """ using 1:8 smooth csplines title "stored heap" """)
    1.13 +                  """ using 1:6 smooth sbezier title "heap maximum (smooth)" """,
    1.14 +                  """ using 1:6 smooth csplines title "heap maximum" """,
    1.15 +                  """ using 1:7 smooth sbezier title "heap average (smooth)" """,
    1.16 +                  """ using 1:7 smooth csplines title "heap average" """,
    1.17 +                  """ using 1:8 smooth sbezier title "heap stored (smooth)" """,
    1.18 +                  """ using 1:8 smooth csplines title "heap stored" """)
    1.19  
    1.20                def jfreechart(plot_name: String, fields: ML_Statistics.Fields): Image =
    1.21                {
    1.22 @@ -548,19 +548,19 @@
    1.23                    HTML.text("timing:") -> HTML.text(session.head.timing.message_resources),
    1.24                    HTML.text("ML timing:") -> HTML.text(session.head.ml_timing.message_resources)) :::
    1.25                  ML_Statistics.mem_print(session.head.maximum_code).map(s =>
    1.26 -                  HTML.text("maximum code:") -> HTML.text(s)).toList :::
    1.27 +                  HTML.text("code maximum:") -> HTML.text(s)).toList :::
    1.28                  ML_Statistics.mem_print(session.head.average_code).map(s =>
    1.29 -                  HTML.text("average code:") -> HTML.text(s)).toList :::
    1.30 +                  HTML.text("code average:") -> HTML.text(s)).toList :::
    1.31                  ML_Statistics.mem_print(session.head.maximum_stack).map(s =>
    1.32 -                  HTML.text("maximum stack:") -> HTML.text(s)).toList :::
    1.33 +                  HTML.text("stack maximum:") -> HTML.text(s)).toList :::
    1.34                  ML_Statistics.mem_print(session.head.average_stack).map(s =>
    1.35 -                  HTML.text("average stack:") -> HTML.text(s)).toList :::
    1.36 +                  HTML.text("stack average:") -> HTML.text(s)).toList :::
    1.37                  ML_Statistics.mem_print(session.head.maximum_heap).map(s =>
    1.38 -                  HTML.text("maximum heap:") -> HTML.text(s)).toList :::
    1.39 +                  HTML.text("heap maximum:") -> HTML.text(s)).toList :::
    1.40                  ML_Statistics.mem_print(session.head.average_heap).map(s =>
    1.41 -                  HTML.text("average heap:") -> HTML.text(s)).toList :::
    1.42 +                  HTML.text("heap average:") -> HTML.text(s)).toList :::
    1.43                  ML_Statistics.mem_print(session.head.stored_heap).map(s =>
    1.44 -                  HTML.text("stored heap:") -> HTML.text(s)).toList :::
    1.45 +                  HTML.text("heap stored:") -> HTML.text(s)).toList :::
    1.46                  proper_string(session.head.isabelle_version).map(s =>
    1.47                    HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
    1.48                  proper_string(session.head.afp_version).map(s =>