tuned signature;
authorwenzelm
Sat May 27 13:01:25 2017 +0200 (2017-05-27)
changeset 659465dd3974cf0bc
parent 65945 35652d0834f4
child 65947 223fd19ac6b3
tuned signature;
src/Pure/Admin/build_status.scala
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat May 27 12:57:57 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sat May 27 13:01:25 2017 +0200
     1.3 @@ -433,8 +433,7 @@
     1.4                  proper_string(session.head.afp_version).map(s =>
     1.5                    HTML.text("AFP version:") -> HTML.text(s)).toList) ::
     1.6                session_plots.getOrElse(session.name, Nil).map(image =>
     1.7 -                HTML.width(image.width / 2)(HTML.height(image.height / 2)(
     1.8 -                  HTML.image(image.name))))))))
     1.9 +                HTML.size(image.width / 2, image.height / 2)(HTML.image(image.name)))))))
    1.10      }
    1.11    }
    1.12  
     2.1 --- a/src/Pure/Thy/html.scala	Sat May 27 12:57:57 2017 +0200
     2.2 +++ b/src/Pure/Thy/html.scala	Sat May 27 13:01:25 2017 +0200
     2.3 @@ -93,9 +93,11 @@
     2.4    { def apply(elem: XML.Elem): XML.Elem = elem + (name -> value) }
     2.5  
     2.6    def id(s: String) = new Attribute("id", s)
     2.7 +  def css_class(name: String) = new Attribute("class", name)
     2.8 +
     2.9    def width(w: Int) = new Attribute("width", w.toString)
    2.10    def height(h: Int) = new Attribute("height", h.toString)
    2.11 -  def css_class(name: String) = new Attribute("class", name)
    2.12 +  def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem))
    2.13  
    2.14  
    2.15    /* structured markup operators */