equal
deleted
inserted
replaced
62 fun print_chr s = |
62 fun print_chr s = |
63 if Symbol.is_char s then |
63 if Symbol.is_char s then |
64 (case ord s of |
64 (case ord s of |
65 34 => "\\\"" |
65 34 => "\\\"" |
66 | 92 => "\\\\" |
66 | 92 => "\\\\" |
|
67 | 7 => "\\a" |
|
68 | 8 => "\\b" |
67 | 9 => "\\t" |
69 | 9 => "\\t" |
68 | 10 => "\\n" |
70 | 10 => "\\n" |
69 | 11 => "\\f" |
71 | 11 => "\\v" |
|
72 | 12 => "\\f" |
70 | 13 => "\\r" |
73 | 13 => "\\r" |
71 | c => |
74 | c => |
72 if c < 32 then "\\^" ^ chr (c + 64) |
75 if c < 32 then "\\^" ^ chr (c + 64) |
73 else if c < 127 then s |
76 else if c < 127 then s |
74 else "\\" ^ string_of_int c) |
77 else "\\" ^ string_of_int c) |