src/Pure/Thy/html.ML
changeset 45666 d83797ef0d2d
parent 43592 e67d104c0c50
child 46866 b190913c3c41
--- a/src/Pure/Thy/html.ML	Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Thy/html.ML	Mon Nov 28 22:05:32 2011 +0100
@@ -49,8 +49,8 @@
 fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
 
 fun span_class (name, props) =
-  (case Markup.get_entity_kind (name, props) of
-    SOME kind => Markup.entityN ^ "_" ^ name
+  (case Isabelle_Markup.get_entity_kind (name, props) of
+    SOME kind => Isabelle_Markup.entityN ^ "_" ^ name
   | NONE => name);
 
 val _ = Markup.add_mode htmlN (span o span_class);
@@ -59,7 +59,7 @@
 (* symbol output *)
 
 local
-  val hidden = span Markup.hiddenN |-> enclose;
+  val hidden = span Isabelle_Markup.hiddenN |-> enclose;
 
   (* FIXME proper unicode -- produced on Scala side *)
   val html_syms = Symtab.make