src/Pure/Admin/build_status.scala
changeset 65773 120ef768c84c
parent 65769 490b7c517000
child 65782 4935bac8a850
     1.1 --- a/src/Pure/Admin/build_status.scala	Mon May 08 14:30:37 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Mon May 08 14:30:59 2017 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  {
     1.5    private val default_target_dir = Path.explode("build_status")
     1.6    private val default_history_length = 30
     1.7 -  private val default_image_size = (640, 480)
     1.8 +  private val default_image_size = (800, 600)
     1.9  
    1.10  
    1.11    /* data profiles */
    1.12 @@ -253,7 +253,10 @@
    1.13                    HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
    1.14                    HTML.bold(HTML.text("ML timing: ")) ::
    1.15                      HTML.text(session.ml_timing.message_resources))) ::
    1.16 -                session_plots.getOrElse(session.name, Nil).map(HTML.image(_)))))))
    1.17 +                session_plots.getOrElse(session.name, Nil).map(plot_name =>
    1.18 +                  HTML.image(plot_name) +
    1.19 +                    HTML.width(image_size._1 / 2) +
    1.20 +                    HTML.height(image_size._2 / 2)))))))
    1.21      }
    1.22  
    1.23      File.write(target_dir + Path.basic("index.html"),