49 (* SOME x => (sym_width s, UnicodeSymbols.utf8 [x]) (* utf-8 *) *) |
49 (* SOME x => (sym_width s, UnicodeSymbols.utf8 [x]) (* utf-8 *) *) |
50 | NONE => (size s, XML.text s)); |
50 | NONE => (size s, XML.text s)); |
51 |
51 |
52 fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s); |
52 fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s); |
53 fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s); |
53 fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s); |
54 fun output_loc s = apsnd (enclose "<span class=\"loc\">" "</span>") (output_sym s); |
|
55 |
54 |
56 fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss |
55 fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss |
57 | output_syms ("\<^isub>" :: s :: ss) = output_sub s :: output_syms ss |
56 | output_syms ("\<^isub>" :: s :: ss) = output_sub s :: output_syms ss |
58 | output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss |
57 | output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss |
59 | output_syms ("\<^isup>" :: s :: ss) = output_sup s :: output_syms ss |
58 | output_syms ("\<^isup>" :: s :: ss) = output_sup s :: output_syms ss |
60 | output_syms ("\<^loc>" :: s :: ss) = output_loc s :: output_syms ss |
|
61 | output_syms (s :: ss) = output_sym s :: output_syms ss |
59 | output_syms (s :: ss) = output_sym s :: output_syms ss |
62 | output_syms [] = []; |
60 | output_syms [] = []; |
63 |
61 |
64 fun output_width str = |
62 fun output_width str = |
65 if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str) |
63 if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str) |