equal
deleted
inserted
replaced
50 |
50 |
51 fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s); |
51 fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s); |
52 fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s); |
52 fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s); |
53 |
53 |
54 fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss |
54 fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss |
55 | output_syms ("\<^isub>" :: s :: ss) = output_sub s :: output_syms ss |
|
56 | output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss |
55 | output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss |
57 | output_syms ("\<^isup>" :: s :: ss) = output_sup s :: output_syms ss |
|
58 | output_syms (s :: ss) = output_sym s :: output_syms ss |
56 | output_syms (s :: ss) = output_sym s :: output_syms ss |
59 | output_syms [] = []; |
57 | output_syms [] = []; |
60 |
58 |
61 fun output_width str = |
59 fun output_width str = |
62 if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str) |
60 if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str) |