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