equal
deleted
inserted
replaced
39 |
39 |
40 fun xsym_output "\\" = "\\\\" |
40 fun xsym_output "\\" = "\\\\" |
41 | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s; |
41 | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s; |
42 |
42 |
43 fun xsymbols_output s = |
43 fun xsymbols_output s = |
44 if print_mode_active Symbol.xsymbolsN andalso exists_string (equal "\\") s then |
44 if print_mode_active Symbol.xsymbolsN andalso exists_string (fn c => c = "\\") s then |
45 let val syms = Symbol.explode s |
45 let val syms = Symbol.explode s |
46 in (implode (map xsym_output syms), Symbol.length syms) end |
46 in (implode (map xsym_output syms), Symbol.length syms) end |
47 else Output.default_output s; |
47 else Output.default_output s; |
48 |
48 |
49 in |
49 in |