# HG changeset patch
# User wenzelm
# Date 1495882885 -7200
# Node ID 5dd3974cf0bc7271c34d805e2e5134146fb3343a
# Parent  35652d0834f49b4c2cf373989ca68a273bcab2e8
tuned signature;

diff -r 35652d0834f4 -r 5dd3974cf0bc src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat May 27 12:57:57 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Sat May 27 13:01:25 2017 +0200
@@ -433,8 +433,7 @@
                 proper_string(session.head.afp_version).map(s =>
                   HTML.text("AFP version:") -> HTML.text(s)).toList) ::
               session_plots.getOrElse(session.name, Nil).map(image =>
-                HTML.width(image.width / 2)(HTML.height(image.height / 2)(
-                  HTML.image(image.name))))))))
+                HTML.size(image.width / 2, image.height / 2)(HTML.image(image.name)))))))
     }
   }
 
diff -r 35652d0834f4 -r 5dd3974cf0bc src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sat May 27 12:57:57 2017 +0200
+++ b/src/Pure/Thy/html.scala	Sat May 27 13:01:25 2017 +0200
@@ -93,9 +93,11 @@
   { def apply(elem: XML.Elem): XML.Elem = elem + (name -> value) }
 
   def id(s: String) = new Attribute("id", s)
+  def css_class(name: String) = new Attribute("class", name)
+
   def width(w: Int) = new Attribute("width", w.toString)
   def height(h: Int) = new Attribute("height", h.toString)
-  def css_class(name: String) = new Attribute("class", name)
+  def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem))
 
 
   /* structured markup operators */