src/Pure/Thy/html.ML

--- a/src/Pure/Thy/html.ML	Fri Dec 04 22:51:59 2009 +0100
+++ b/src/Pure/Thy/html.ML	Sat Dec 05 16:39:49 2009 +0100
@@ -45,9 +45,18 @@
 fun html_mode f x = PrintMode.with_modes [htmlN] f x;
 
 
+(* common markup *)
+
+fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
+
+val _ = Markup.add_mode htmlN (fn (name, _) => span name);
+
+
 (* symbol output *)
 
 local
+  val hidden = XML.text #> (span Markup.hiddenN |-> enclose);
+
   val html_syms = Symtab.make
    [("'", (1, "&#39;")),
     ("\\<spacespace>", (2, "&nbsp;&nbsp;")),
@@ -190,10 +199,10 @@
     ("\\<longleftrightarrow>", (3, "&lt;-&gt;")),
     ("\\<longrightarrow>", (3, "--&gt;")),
     ("\\<rightarrow>", (2, "-&gt;")),
-    ("\\<^bsub>", (0, "<sub>")),
-    ("\\<^esub>", (0, "</sub>")),
-    ("\\<^bsup>", (0, "<sup>")),
-    ("\\<^esup>", (0, "</sup>"))];
+    ("\\<^bsub>", (0, hidden "\\<^bsub>" ^ "<sub>")),
+    ("\\<^esub>", (0, hidden "\\<^esub>" ^ "</sub>")),
+    ("\\<^bsup>", (0, hidden "\\<^bsup>" ^ "<sup>")),
+    ("\\<^esup>", (0, hidden "\\<^esup>" ^ "</sup>"))];
 
   fun output_sym s =
     if Symbol.is_raw s then (1, Symbol.decode_raw s)
@@ -202,15 +211,21 @@
         SOME x => x
       | NONE => (size s, XML.text s));
 
-  fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
-  fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s);
-  fun output_loc s = apsnd (enclose "<span class=\"loc\">" "</span>") (output_sym s);
+  fun output_markup (bg, en) s1 s2 =
+    let val (n, txt) = output_sym s2
+    in (n, hidden s1 ^ enclose bg en txt) end;
 
-  fun output_syms ("\\<^sub>" :: s :: ss) = output_sub s :: output_syms ss
-    | output_syms ("\\<^isub>" :: s :: ss) = output_sub s :: output_syms ss
-    | output_syms ("\\<^sup>" :: s :: ss) = output_sup s :: output_syms ss
-    | output_syms ("\\<^isup>" :: s :: ss) = output_sup s :: output_syms ss
-    | output_syms ("\\<^loc>" :: s :: ss) = output_loc s :: output_syms ss
+  val output_sub = output_markup ("<sub>", "</sub>");
+  val output_sup = output_markup ("<sup>", "</sup>");
+  val output_bold = output_markup (span "bold");
+  val output_loc = output_markup (span "loc");
+
+  fun output_syms (s1 :: s2 :: ss) =
+        if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then output_sub s1 s2 :: output_syms ss
+        else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then output_sup s1 s2 :: output_syms ss
+        else if s1 = "\\<^bold>" then output_bold s1 s2 :: output_syms ss
+        else if s1 = "\\<^loc>" then output_loc s1 s2 :: output_syms ss
+        else output_sym s1 :: output_syms (s2 :: ss)
     | output_syms (s :: ss) = output_sym s :: output_syms ss
     | output_syms [] = [];
 in
@@ -230,13 +245,6 @@
 end;
 
 
-(* common markup *)
-
-fun span s = ("<span class=" ^ quote (XML.text s) ^ ">", "</span>");
-
-val _ = Markup.add_mode htmlN (fn (name, _) => span name);
-
-
 
 (** HTML markup **)