--- a/src/Pure/Thy/html.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Thy/html.scala Mon Nov 28 22:05:32 2011 +0100
@@ -49,7 +49,7 @@
XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
def hidden(txt: String): XML.Elem =
- span(Markup.HIDDEN, List(XML.Text(txt)))
+ span(Isabelle_Markup.HIDDEN, List(XML.Text(txt)))
def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
@@ -61,7 +61,7 @@
tree match {
case XML.Elem(m @ Markup(name, props), ts) =>
val span_class =
- m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name }
+ m match { case Isabelle_Markup.Entity(kind, _) => name + "_" + kind case _ => name }
val html_span = span(span_class, ts.flatMap(html_spans))
if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
else List(html_span)