equal
deleted
inserted
replaced
202 ("\\<^esup>", (0.0, "</sup>"))]; |
202 ("\\<^esup>", (0.0, "</sup>"))]; |
203 |
203 |
204 val escape = fn "<" => "<" | ">" => ">" | "&" => "&" | c => c; |
204 val escape = fn "<" => "<" | ">" => ">" | "&" => "&" | c => c; |
205 |
205 |
206 fun output_sym s = |
206 fun output_sym s = |
207 if Symbol.is_raw s then (1.0, Symbol.decode_raw s) |
207 (case Symtab.lookup html_syms s of |
208 else |
208 SOME x => x |
209 (case Symtab.lookup html_syms s of SOME x => x |
209 | NONE => (real (size s), translate_string escape s)); |
210 | NONE => (real (size s), translate_string escape s)); |
|
211 |
210 |
212 fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s); |
211 fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s); |
213 fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s); |
212 fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s); |
214 fun output_loc s = apsnd (enclose "<span class=\"loc\">" "</span>") (output_sym s); |
213 fun output_loc s = apsnd (enclose "<span class=\"loc\">" "</span>") (output_sym s); |
215 |
214 |