--- a/src/Pure/Thy/html.scala Sun Oct 23 13:16:23 2016 +0200
+++ b/src/Pure/Thy/html.scala Sun Oct 23 15:24:10 2016 +0200
@@ -81,27 +81,66 @@
def output(tree: XML.Tree): String = output(List(tree))
- /* markup operators */
+ /* structured markup operators */
+
+ def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
+
+ class Operator(name: String)
+ { def apply(body: XML.Body): XML.Elem = XML.elem(name, body) }
- type Operator = XML.Body => XML.Elem
+ 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 par = new Operator("p")
+ val emph = new Operator("em")
+ val bold = new Operator("b")
- val chapter: Operator = XML.elem("h1", _)
- val section: Operator = XML.elem("h2", _)
- val subsection: Operator = XML.elem("h3", _)
- val subsubsection: Operator = XML.elem("h4", _)
- val paragraph: Operator = XML.elem("h5", _)
- val subparagraph: Operator = XML.elem("h6", _)
+ 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 =
+ XML.elem("ul", items.map(XML.elem("li", _)))
+
+ def enumerate(items: List[XML.Body]): XML.Elem =
+ XML.elem("ol", items.map(XML.elem("li", _)))
+
+ 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)
/* document */
+ val header: String =
+ """<?xml version="1.0" encoding="utf-8" ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">"""
+
+ val head_meta: XML.Elem =
+ XML.Elem(Markup("meta",
+ List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
+
+ def output_document(head: XML.Body, body: XML.Body): String =
+ cat_lines(
+ List(header,
+ output(XML.elem("head", head_meta :: head)),
+ output(XML.elem("body", body))))
+
+
+ /* Isabelle document */
+
def begin_document(title: String): String =
- "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" +
- "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " +
- "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" +
- "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" +
- "<head>\n" +
- "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" +
+ header + "\n" +
+ "<head>\n" + output(head_meta) + "\n" +
"<title>" + output(title + " (" + Distribution.version + ")") + "</title>\n" +
"<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" +
"</head>\n" +