# HG changeset patch
# User wenzelm
# Date 1477229050 -7200
# Node ID 27739e1d7978891dbadb5efd2cad2afddae77a2e
# Parent 15c90b744481f53b5348e384dab5ee9a8e39462b
more operations;
diff -r 15c90b744481 -r 27739e1d7978 src/Pure/Thy/html.scala
--- 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 =
+ """
+
+"""
+
+ 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 =
- "\n" +
- "\n" +
- "\n" +
- "\n" +
- "\n" +
+ header + "\n" +
+ "\n" + output(head_meta) + "\n" +
"" + output(title + " (" + Distribution.version + ")") + "\n" +
"\n" +
"\n" +