clarified signature;
authorwenzelm
Sat May 27 12:33:14 2017 +0200 (2017-05-27)
changeset 65942864a4892e43c
parent 65941 316c30b60ebc
child 65943 bf55ad5eaf75
clarified signature;
src/Pure/Admin/build_status.scala
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat May 27 00:30:48 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sat May 27 12:33:14 2017 +0200
     1.3 @@ -110,9 +110,9 @@
     1.4        if (errors.isEmpty) HTML.text(name + " (" + isabelle_version + ")")
     1.5        else {
     1.6          val tooltip_errors =
     1.7 -          errors.map(msg => HTML.pre(HTML.text(Symbol.decode(msg))) + HTML.error_message_class)
     1.8 -        val tooltip = List(HTML.div(tooltip_errors) + HTML.tooltip_class)
     1.9 -        HTML.span(HTML.text(name) ::: tooltip) + HTML.error_class ::
    1.10 +          errors.map(msg => HTML.error_message_class(HTML.pre(HTML.text(Symbol.decode(msg)))))
    1.11 +        val tooltip = List(HTML.tooltip_class(HTML.div(tooltip_errors)))
    1.12 +        HTML.error_class(HTML.span(HTML.text(name) ::: tooltip)) ::
    1.13          HTML.text(" (" + isabelle_version + ")")
    1.14        }
    1.15    }
    1.16 @@ -277,7 +277,7 @@
    1.17                case Nil => Nil
    1.18                case sessions =>
    1.19                  HTML.break :::
    1.20 -                List(HTML.span(HTML.text("Failed sessions:")) + HTML.error_message_class) :::
    1.21 +                List(HTML.error_message_class(HTML.span(HTML.text("Failed sessions:")))) :::
    1.22                  List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
    1.23              })
    1.24            }))))))
    1.25 @@ -420,7 +420,7 @@
    1.26                HTML.text(" (" + session.head.timing.message_resources + ")"))))) ::
    1.27          data_entry.sessions.flatMap(session =>
    1.28            List(
    1.29 -            HTML.section(session.name) + HTML.id("session_" + session.name),
    1.30 +            HTML.id("session_" + session.name)(HTML.section(session.name)),
    1.31              HTML.par(
    1.32                HTML.description(
    1.33                  List(
    1.34 @@ -437,9 +437,8 @@
    1.35                  proper_string(session.head.afp_version).map(s =>
    1.36                    HTML.text("AFP version:") -> HTML.text(s)).toList) ::
    1.37                session_plots.getOrElse(session.name, Nil).map(image =>
    1.38 -                HTML.image(image.name) +
    1.39 -                  HTML.width(image.width / 2) +
    1.40 -                  HTML.height(image.height / 2))))))
    1.41 +                HTML.width(image.width / 2)(HTML.height(image.height / 2)(
    1.42 +                  HTML.image(image.name))))))))
    1.43      }
    1.44    }
    1.45  
     2.1 --- a/src/Pure/Thy/html.scala	Sat May 27 00:30:48 2017 +0200
     2.2 +++ b/src/Pure/Thy/html.scala	Sat May 27 12:33:14 2017 +0200
     2.3 @@ -89,10 +89,13 @@
     2.4  
     2.5    /* attributes */
     2.6  
     2.7 -  def id(s: String): XML.Attribute = ("id" -> s)
     2.8 -  def width(w: Int): XML.Attribute = ("width" -> w.toString)
     2.9 -  def height(h: Int): XML.Attribute = ("height" -> h.toString)
    2.10 -  def css_class(name: String): XML.Attribute = ("class" -> name)
    2.11 +  class Attribute(name: String, value: String)
    2.12 +  { def apply(elem: XML.Elem): XML.Elem = elem + (name -> value) }
    2.13 +
    2.14 +  def id(s: String) = new Attribute("id", s)
    2.15 +  def width(w: Int) = new Attribute("width", w.toString)
    2.16 +  def height(h: Int) = new Attribute("height", h.toString)
    2.17 +  def css_class(name: String) = new Attribute("class", name)
    2.18  
    2.19  
    2.20    /* structured markup operators */
    2.21 @@ -143,17 +146,17 @@
    2.22    /* messages */
    2.23  
    2.24    // background
    2.25 -  val writeln_message_class: XML.Attribute = css_class("writeln_message")
    2.26 -  val warning_message_class: XML.Attribute = css_class("warning_message")
    2.27 -  val error_message_class: XML.Attribute = css_class("error_message")
    2.28 +  val writeln_message_class: Attribute = css_class("writeln_message")
    2.29 +  val warning_message_class: Attribute = css_class("warning_message")
    2.30 +  val error_message_class: Attribute = css_class("error_message")
    2.31  
    2.32    // underline
    2.33 -  val writeln_class: XML.Attribute = css_class("writeln")
    2.34 -  val warning_class: XML.Attribute = css_class("warning")
    2.35 -  val error_class: XML.Attribute = css_class("error")
    2.36 +  val writeln_class: Attribute = css_class("writeln")
    2.37 +  val warning_class: Attribute = css_class("warning")
    2.38 +  val error_class: Attribute = css_class("error")
    2.39  
    2.40    // tooltips
    2.41 -  val tooltip_class: XML.Attribute = css_class("tooltip")
    2.42 +  val tooltip_class: Attribute = css_class("tooltip")
    2.43  
    2.44  
    2.45    /* document */