# HG changeset patch
# User wenzelm
# Date 1494246659 -7200
# Node ID 120ef768c84ce8bc514d2fc9dc683eff314e5c48
# Parent  368399c5d87f99c7061fe92e7cac215dad91f378
clarified image size;

diff -r 368399c5d87f -r 120ef768c84c src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Mon May 08 14:30:37 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Mon May 08 14:30:59 2017 +0200
@@ -11,7 +11,7 @@
 {
   private val default_target_dir = Path.explode("build_status")
   private val default_history_length = 30
-  private val default_image_size = (640, 480)
+  private val default_image_size = (800, 600)
 
 
   /* data profiles */
@@ -253,7 +253,10 @@
                   HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
                   HTML.bold(HTML.text("ML timing: ")) ::
                     HTML.text(session.ml_timing.message_resources))) ::
-                session_plots.getOrElse(session.name, Nil).map(HTML.image(_)))))))
+                session_plots.getOrElse(session.name, Nil).map(plot_name =>
+                  HTML.image(plot_name) +
+                    HTML.width(image_size._1 / 2) +
+                    HTML.height(image_size._2 / 2)))))))
     }
 
     File.write(target_dir + Path.basic("index.html"),
diff -r 368399c5d87f -r 120ef768c84c src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Mon May 08 14:30:37 2017 +0200
+++ b/src/Pure/Thy/html.scala	Mon May 08 14:30:59 2017 +0200
@@ -83,7 +83,9 @@
 
   /* attributes */
 
-  def id(s: String): Properties.Entry = ("id" -> s)
+  def id(s: String): XML.Attribute = ("id" -> s)
+  def width(w: Int): XML.Attribute = ("width" -> w.toString)
+  def height(h: Int): XML.Attribute = ("height" -> h.toString)
 
 
   /* structured markup operators */