equal
deleted
inserted
replaced
81 ("|", "{\\isacharbar}"), |
81 ("|", "{\\isacharbar}"), |
82 ("}", "{\\isacharbraceright}"), |
82 ("}", "{\\isacharbraceright}"), |
83 ("~", "{\\isachartilde}")]; |
83 ("~", "{\\isachartilde}")]; |
84 |
84 |
85 fun output_chr " " = "\\ " |
85 fun output_chr " " = "\\ " |
|
86 | output_chr "\t" = "\\ " |
86 | output_chr "\n" = "\\isanewline\n" |
87 | output_chr "\n" = "\\isanewline\n" |
87 | output_chr c = |
88 | output_chr c = |
88 (case Symtab.lookup char_table c of |
89 (case Symtab.lookup char_table c of |
89 SOME s => enclose_literal c s |
90 SOME s => enclose_literal c s |
90 | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c); |
91 | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c); |