tuned signature;
authorwenzelm
Thu Jun 01 15:19:50 2017 +0200 (2017-06-01)
changeset 6599250daca61efd6
parent 65991 fa787e233214
child 65993 75590c9a585f
tuned signature;
src/Pure/Admin/build_status.scala
src/Pure/Thy/html.scala
src/Pure/Thy/present.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Thu Jun 01 12:27:20 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Thu Jun 01 15:19:50 2017 +0200
     1.3 @@ -273,7 +273,7 @@
     1.4                case Nil => Nil
     1.5                case sessions =>
     1.6                  HTML.break :::
     1.7 -                List(HTML.error_message(HTML.span(HTML.text("Failed sessions:")))) :::
     1.8 +                List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) :::
     1.9                  List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
    1.10              })
    1.11            }))))))
    1.12 @@ -416,7 +416,7 @@
    1.13                HTML.text(" (" + session.head.timing.message_resources + ")"))))) ::
    1.14          data_entry.sessions.flatMap(session =>
    1.15            List(
    1.16 -            HTML.id("session_" + session.name)(HTML.section(session.name)),
    1.17 +            HTML.section(HTML.id("session_" + session.name), session.name),
    1.18              HTML.par(
    1.19                HTML.description(
    1.20                  List(
     2.1 --- a/src/Pure/Thy/html.scala	Thu Jun 01 12:27:20 2017 +0200
     2.2 +++ b/src/Pure/Thy/html.scala	Thu Jun 01 15:19:50 2017 +0200
     2.3 @@ -82,14 +82,17 @@
     2.4  
     2.5    /* attributes */
     2.6  
     2.7 -  class Attribute(name: String, value: String)
     2.8 -  { def apply(elem: XML.Elem): XML.Elem = elem + (name -> value) }
     2.9 +  class Attribute(val name: String, value: String)
    2.10 +  {
    2.11 +    def xml: XML.Attribute = name -> value
    2.12 +    def apply(elem: XML.Elem): XML.Elem = elem + xml
    2.13 +  }
    2.14  
    2.15 -  def id(s: String) = new Attribute("id", s)
    2.16 -  def css_class(name: String) = new Attribute("class", name)
    2.17 +  def id(s: String): Attribute = new Attribute("id", s)
    2.18 +  def css_class(name: String): Attribute = new Attribute("class", name)
    2.19  
    2.20 -  def width(w: Int) = new Attribute("width", w.toString)
    2.21 -  def height(h: Int) = new Attribute("height", h.toString)
    2.22 +  def width(w: Int): Attribute = new Attribute("width", w.toString)
    2.23 +  def height(h: Int): Attribute = new Attribute("height", h.toString)
    2.24    def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem))
    2.25  
    2.26  
    2.27 @@ -98,11 +101,19 @@
    2.28    def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
    2.29    val break: XML.Body = List(XML.elem("br"))
    2.30  
    2.31 -  class Operator(name: String)
    2.32 -  { def apply(body: XML.Body): XML.Elem = XML.elem(name, body) }
    2.33 +  class Operator(val name: String)
    2.34 +  {
    2.35 +    def apply(body: XML.Body): XML.Elem = XML.elem(name, body)
    2.36 +    def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body))
    2.37 +    def apply(c: String, body: XML.Body): XML.Elem = apply(css_class(c), body)
    2.38 +  }
    2.39  
    2.40    class Heading(name: String) extends Operator(name)
    2.41 -  { def apply(txt: String): XML.Elem = super.apply(text(txt)) }
    2.42 +  {
    2.43 +    def apply(txt: String): XML.Elem = super.apply(text(txt))
    2.44 +    def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt))
    2.45 +    def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt))
    2.46 +  }
    2.47  
    2.48    val div = new Operator("div")
    2.49    val span = new Operator("span")
    2.50 @@ -135,7 +146,7 @@
    2.51    def image(src: String, alt: String = ""): XML.Elem =
    2.52      XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
    2.53  
    2.54 -  def source(src: String): XML.Elem = css_class("source")(div(List(pre(text(src)))))
    2.55 +  def source(src: String): XML.Elem = div("source", List(pre(text(src))))
    2.56  
    2.57    def style(s: String): XML.Elem = XML.elem("style", text(s))
    2.58  
    2.59 @@ -156,7 +167,7 @@
    2.60    /* tooltips */
    2.61  
    2.62    def tooltip(item: XML.Body, tip: XML.Body): XML.Elem =
    2.63 -    span(item ::: List(css_class("tooltip")(div(tip))))
    2.64 +    span(item ::: List(div("tooltip", tip)))
    2.65  
    2.66    def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem =
    2.67      HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg)))))
     3.1 --- a/src/Pure/Thy/present.scala	Thu Jun 01 12:27:20 2017 +0200
     3.2 +++ b/src/Pure/Thy/present.scala	Thu Jun 01 15:19:50 2017 +0200
     3.3 @@ -52,12 +52,12 @@
     3.4        HTML.chapter(title) ::
     3.5         (if (sessions.isEmpty) Nil
     3.6          else
     3.7 -          List(HTML.css_class("sessions")(HTML.div(List(
     3.8 -            HTML.description(
     3.9 +          List(HTML.div("sessions",
    3.10 +            List(HTML.description(
    3.11                sessions.map({ case (name, description) =>
    3.12                  (List(HTML.link(name + "/index.html", HTML.text(name))),
    3.13                    if (description == "") Nil
    3.14 -                  else List(HTML.pre(HTML.text(description)))) }))))))))
    3.15 +                  else List(HTML.pre(HTML.text(description)))) })))))))
    3.16    }
    3.17  
    3.18    def make_global_index(browser_info: Path)