src/Pure/Thy/html.scala

 
   def output(body: XML.Body): String = Library.make_string(output(body, _))
   def output(tree: XML.Tree): String = output(List(tree))
 
 
+  /* attributes */
+
+  def id(s: String): Properties.Entry = ("id" -> s)
+
+
   /* 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"))
 
   class Operator(name: String)
   { def apply(body: XML.Body): XML.Elem = XML.elem(name, body) }
 
   class Heading(name: String) extends Operator(name)
   { def apply(txt: String): XML.Elem = super.apply(text(txt)) }
 
   val div = new Operator("div")
   val span = new Operator("span")
+  val pre = new Operator("pre")
   val par = new Operator("p")
   val emph = new Operator("em")
   val bold = new Operator("b")
 
   val title = new Heading("title")

   def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
     XML.elem("dl", items.flatMap({ case (x, y) => List(XML.elem("dt", x), XML.elem("dd", y)) }))
 
   def link(href: String, body: XML.Body = Nil): XML.Elem =
     XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
+
+  def image(src: String, alt: String = ""): XML.Elem =
+    XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
 
 
   /* document */
 
   val header: String =

   /* common markup elements */
 
   private def session_entry(entry: (String, String)): String =
   {
     val (name, description) = entry
-    val descr =
-      if (description == "") Nil
-      else List(XML.elem("br"), XML.elem("pre", List(XML.Text(description))))
+    val descr = if (description == "") Nil else break ::: List(pre(text(description)))
     XML.string_of_tree(
       XML.elem("li",
         List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
           List(XML.Text(name)))) ::: descr)) + "\n"
   }