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 */