--- a/src/Pure/IsaMakefile Fri Dec 04 18:52:55 2009 +0100
+++ b/src/Pure/IsaMakefile Sat Dec 05 10:18:23 2009 +0100
@@ -128,7 +128,7 @@
System/cygwin.scala System/gui_setup.scala \
System/isabelle_process.scala System/isabelle_syntax.scala \
System/isabelle_system.scala System/platform.scala \
- Thy/completion.scala Thy/thy_header.scala
+ Thy/completion.scala Thy/html.scala Thy/thy_header.scala
JAR_DIR = $(ISABELLE_HOME)/lib/classes
PURE_JAR = $(JAR_DIR)/Pure.jar
--- a/src/Pure/Thy/html.ML Fri Dec 04 18:52:55 2009 +0100
+++ b/src/Pure/Thy/html.ML Sat Dec 05 10:18:23 2009 +0100
@@ -49,7 +49,8 @@
local
val html_syms = Symtab.make
- [("\\<spacespace>", (2, " ")),
+ [("'", (1, "'")),
+ ("\\<spacespace>", (2, " ")),
("\\<exclamdown>", (1, "¡")),
("\\<cent>", (1, "¢")),
("\\<pounds>", (1, "£")),
@@ -197,7 +198,8 @@
fun output_sym s =
if Symbol.is_raw s then (1, Symbol.decode_raw s)
else
- (case Symtab.lookup html_syms s of SOME x => x
+ (case Symtab.lookup html_syms s of
+ SOME x => x
| NONE => (size s, XML.text s));
fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/html.scala Sat Dec 05 10:18:23 2009 +0100
@@ -0,0 +1,41 @@
+/* Title: Pure/Thy/html.scala
+ Author: Makarius
+
+Basic HTML output.
+*/
+
+package isabelle
+
+object HTML
+{
+ // common elements and attributes
+
+ val BODY = "body"
+ val DIV = "div"
+ val SPAN = "span"
+ val BR = "br"
+ val CLASS = "class"
+
+
+ // document markup
+
+ def body(trees: List[XML.Tree]): XML.Tree =
+ XML.Elem(BODY, Nil, trees)
+
+ def div(trees: List[XML.Tree]): XML.Tree =
+ XML.Elem(DIV, Nil, trees)
+
+ val br: XML.Tree = XML.Elem(BR, Nil, Nil)
+
+ def spans(tree: XML.Tree): List[XML.Tree] =
+ tree match {
+ case XML.Elem(name, _, ts) =>
+ List(XML.Elem(SPAN, List((CLASS, name)), ts.flatMap(spans)))
+ case text @ XML.Text(txt) =>
+ txt.split("\n").toList match {
+ case line :: lines if !lines.isEmpty =>
+ XML.Text(line) :: lines.flatMap(l => List(br, XML.Text(l)))
+ case _ => List(text)
+ }
+ }
+}