219 val output_sub = output_markup ("<sub>", "</sub>"); |
219 val output_sub = output_markup ("<sub>", "</sub>"); |
220 val output_sup = output_markup ("<sup>", "</sup>"); |
220 val output_sup = output_markup ("<sup>", "</sup>"); |
221 val output_bold = output_markup (span "bold"); |
221 val output_bold = output_markup (span "bold"); |
222 val output_loc = output_markup (span "loc"); |
222 val output_loc = output_markup (span "loc"); |
223 |
223 |
224 fun output_syms (s1 :: rest) = |
224 fun output_syms [] (result, width) = (implode (rev result), width) |
225 let val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss)) in |
225 | output_syms (s1 :: rest) (result, width) = |
226 if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then output_sub s1 s2 :: output_syms ss |
226 let |
227 else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then output_sup s1 s2 :: output_syms ss |
227 val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss)); |
228 else if s1 = "\\<^bold>" then output_bold s1 s2 :: output_syms ss |
228 val ((w, s), r) = |
229 else if s1 = "\\<^loc>" then output_loc s1 s2 :: output_syms ss |
229 if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then (output_sub s1 s2, ss) |
230 else output_sym s1 :: output_syms rest |
230 else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then (output_sup s1 s2, ss) |
231 end |
231 else if s1 = "\\<^bold>" then (output_bold s1 s2, ss) |
232 | output_syms [] = []; |
232 else if s1 = "\\<^loc>" then (output_loc s1 s2, ss) |
|
233 else (output_sym s1, rest); |
|
234 in output_syms r (s :: result, width + w) end; |
233 in |
235 in |
234 |
236 |
235 fun output_width str = |
237 fun output_width str = output_syms (Symbol.explode str) ([], 0); |
236 let val (syms, width) = |
|
237 fold_map (fn (w, s) => fn width => (s, w + width)) (output_syms (Symbol.explode str)) 0 |
|
238 in (implode syms, width) end; |
|
239 |
|
240 val output = #1 o output_width; |
238 val output = #1 o output_width; |
241 |
239 |
242 val _ = Output.add_mode htmlN output_width Symbol.encode_raw; |
240 val _ = Output.add_mode htmlN output_width Symbol.encode_raw; |
243 |
241 |
244 end; |
242 end; |