# HG changeset patch
# User wenzelm
# Date 1494165859 -7200
# Node ID 787e5ee6ef53b5f63ffe8511cd053208f892487c
# Parent  ed7b5cd3a7f220fb9833436cd125829ad8530fea
more operations;
tuned;

diff -r ed7b5cd3a7f2 -r 787e5ee6ef53 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun May 07 13:42:20 2017 +0200
+++ b/src/Pure/PIDE/markup.scala	Sun May 07 16:04:19 2017 +0200
@@ -634,4 +634,7 @@
   def update_properties(more_props: Properties.T): Markup =
     if (more_props.isEmpty) this
     else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) })
+
+  def + (entry: Properties.Entry): Markup =
+    Markup(name, Properties.put(properties, entry))
 }
diff -r ed7b5cd3a7f2 -r 787e5ee6ef53 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sun May 07 13:42:20 2017 +0200
+++ b/src/Pure/PIDE/xml.scala	Sun May 07 16:04:19 2017 +0200
@@ -18,6 +18,7 @@
 
   /* datatype representation */
 
+  type Attribute = Properties.Entry
   type Attributes = Properties.T
 
   sealed abstract class Tree { override def toString: String = string_of_tree(this) }
@@ -25,9 +26,12 @@
   case class Elem(markup: Markup, body: Body) extends Tree
   {
     def name: String = markup.name
+
     def update_attributes(more_attributes: Attributes): Elem =
       if (more_attributes.isEmpty) this
       else Elem(markup.update_properties(more_attributes), body)
+
+    def + (att: Attribute): Tree = Elem(markup + att, body)
   }
   case class Text(content: String) extends Tree
 
diff -r ed7b5cd3a7f2 -r 787e5ee6ef53 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun May 07 13:42:20 2017 +0200
+++ b/src/Pure/Thy/html.scala	Sun May 07 16:04:19 2017 +0200
@@ -81,9 +81,15 @@
   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) }
@@ -93,6 +99,7 @@
 
   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")
@@ -117,6 +124,9 @@
   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 */
 
@@ -157,9 +167,7 @@
   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"))),