# HG changeset patch
# User wenzelm
# Date 1612031594 -3600
# Node ID 1ab0e1159e7c3a0720e2a22944e23d2846ea1087
# Parent  3d881c1531f38587971effc6fa0744208c92d56b
clarified signature: proper order;

diff -r 3d881c1531f3 -r 1ab0e1159e7c src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sat Jan 30 19:29:22 2021 +0100
+++ b/src/Pure/Thy/html.scala	Sat Jan 30 19:33:14 2021 +0100
@@ -9,20 +9,106 @@
 
 object HTML
 {
+  /* attributes */
+
+  class Attribute(val name: String, value: String)
+  {
+    def xml: XML.Attribute = name -> value
+    def apply(elem: XML.Elem): XML.Elem = elem + xml
+  }
+
+  def id(s: String): Attribute = new Attribute("id", s)
+  def class_(name: String): Attribute = new Attribute("class", name)
+
+  def width(w: Int): Attribute = new Attribute("width", w.toString)
+  def height(h: Int): Attribute = new Attribute("height", h.toString)
+  def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem))
+
+
+  /* structured markup operators */
+
+  def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
+  val break: XML.Body = List(XML.elem("br"))
+  val nl: XML.Body = List(XML.Text("\n"))
+
+  class Operator(val name: String)
+  {
+    def apply(body: XML.Body): XML.Elem = XML.elem(name, body)
+    def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body))
+    def apply(c: String, body: XML.Body): XML.Elem = apply(class_(c), body)
+  }
+
+  class Heading(name: String) extends Operator(name)
+  {
+    def apply(txt: String): XML.Elem = super.apply(text(txt))
+    def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt))
+    def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt))
+  }
+
+  val div = new Operator("div")
+  val span = new Operator("span")
+  val pre = new Operator("pre")
+  val par = new Operator("p")
+  val sub = new Operator("sub")
+  val sup = new Operator("sup")
+  val emph = new Operator("em")
+  val bold = new Operator("b")
+  val code = new Operator("code")
+  val item = new Operator("li")
+  val list = new Operator("ul")
+  val enum = new Operator("ol")
+  val descr = new Operator("dl")
+  val dt = new Operator("dt")
+  val dd = new Operator("dd")
+
+  val title = new Heading("title")
+  val chapter = new Heading("h1")
+  val section = new Heading("h2")
+  val subsection = new Heading("h3")
+  val subsubsection = new Heading("h4")
+  val paragraph = new Heading("h5")
+  val subparagraph = new Heading("h6")
+
+  def itemize(items: List[XML.Body]): XML.Elem = list(items.map(item(_)))
+  def enumerate(items: List[XML.Body]): XML.Elem = enum(items.map(item(_)))
+  def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
+    descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) }))
+
+  def link(href: String, body: XML.Body): XML.Elem =
+    XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
+
+  def link(path: Path, body: XML.Body): XML.Elem = link(path.implode, body)
+
+  def image(src: String, alt: String = ""): XML.Elem =
+    XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
+
+  def source(body: XML.Body): XML.Elem = pre("source", body)
+  def source(src: String): XML.Elem = source(text(src))
+
+  def style(s: String): XML.Elem = XML.elem("style", text(s))
+  def style_file(href: String): XML.Elem =
+    XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
+  def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file))
+
+  def script(s: String): XML.Elem = XML.elem("script", text(s))
+  def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil)
+  def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
+
+
   /* output text with control symbols */
 
-  private lazy val control =
+  private val control =
     Map(
       Symbol.sub -> sub, Symbol.sub_decoded -> sub,
       Symbol.sup -> sup, Symbol.sup_decoded -> sup,
       Symbol.bold -> bold, Symbol.bold_decoded -> bold)
 
-  private lazy val control_block_begin =
+  private val control_block_begin =
     Map(
       Symbol.bsub -> sub, Symbol.bsub_decoded -> sub,
       Symbol.bsup -> sup, Symbol.bsup_decoded -> sup)
 
-  private lazy val control_block_end =
+  private val control_block_end =
     Map(
       Symbol.esub -> sub, Symbol.esub_decoded -> sub,
       Symbol.esup -> sup, Symbol.esup_decoded -> sup)
@@ -118,92 +204,6 @@
     output(List(tree), hidden, structural)
 
 
-  /* attributes */
-
-  class Attribute(val name: String, value: String)
-  {
-    def xml: XML.Attribute = name -> value
-    def apply(elem: XML.Elem): XML.Elem = elem + xml
-  }
-
-  def id(s: String): Attribute = new Attribute("id", s)
-  def class_(name: String): Attribute = new Attribute("class", name)
-
-  def width(w: Int): Attribute = new Attribute("width", w.toString)
-  def height(h: Int): Attribute = new Attribute("height", h.toString)
-  def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem))
-
-
-  /* structured markup operators */
-
-  def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
-  val break: XML.Body = List(XML.elem("br"))
-  val nl: XML.Body = List(XML.Text("\n"))
-
-  class Operator(val name: String)
-  {
-    def apply(body: XML.Body): XML.Elem = XML.elem(name, body)
-    def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body))
-    def apply(c: String, body: XML.Body): XML.Elem = apply(class_(c), body)
-  }
-
-  class Heading(name: String) extends Operator(name)
-  {
-    def apply(txt: String): XML.Elem = super.apply(text(txt))
-    def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt))
-    def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt))
-  }
-
-  val div = new Operator("div")
-  val span = new Operator("span")
-  val pre = new Operator("pre")
-  val par = new Operator("p")
-  val sub = new Operator("sub")
-  val sup = new Operator("sup")
-  val emph = new Operator("em")
-  val bold = new Operator("b")
-  val code = new Operator("code")
-  val item = new Operator("li")
-  val list = new Operator("ul")
-  val enum = new Operator("ol")
-  val descr = new Operator("dl")
-  val dt = new Operator("dt")
-  val dd = new Operator("dd")
-
-  val title = new Heading("title")
-  val chapter = new Heading("h1")
-  val section = new Heading("h2")
-  val subsection = new Heading("h3")
-  val subsubsection = new Heading("h4")
-  val paragraph = new Heading("h5")
-  val subparagraph = new Heading("h6")
-
-  def itemize(items: List[XML.Body]): XML.Elem = list(items.map(item(_)))
-  def enumerate(items: List[XML.Body]): XML.Elem = enum(items.map(item(_)))
-  def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
-    descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) }))
-
-  def link(href: String, body: XML.Body): XML.Elem =
-    XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
-
-  def link(path: Path, body: XML.Body): XML.Elem = link(path.implode, body)
-
-  def image(src: String, alt: String = ""): XML.Elem =
-    XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
-
-  def source(body: XML.Body): XML.Elem = pre("source", body)
-  def source(src: String): XML.Elem = source(text(src))
-
-  def style(s: String): XML.Elem = XML.elem("style", text(s))
-  def style_file(href: String): XML.Elem =
-    XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
-  def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file))
-
-  def script(s: String): XML.Elem = XML.elem("script", text(s))
-  def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil)
-  def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
-
-
   /* messages */
 
   // background