equal
deleted
inserted
replaced
27 case 9 => "\\t" |
27 case 9 => "\\t" |
28 case 10 => "\\n" |
28 case 10 => "\\n" |
29 case 12 => "\\f" |
29 case 12 => "\\f" |
30 case 13 => "\\r" |
30 case 13 => "\\r" |
31 case _ => |
31 case _ => |
32 if (c < 0) "\\" + Library.signed_string_of_int(256 + c) |
32 if (c < 0) "\\" + Value.Int(256 + c) |
33 else if (c < 32) new String(Array[Char](92, 94, (c + 64).toChar)) |
33 else if (c < 32) new String(Array[Char](92, 94, (c + 64).toChar)) |
34 else if (c < 127) Symbol.ascii(c.toChar) |
34 else if (c < 127) Symbol.ascii(c.toChar) |
35 else "\\" + Library.signed_string_of_int(c) |
35 else "\\" + Value.Int(c) |
36 } |
36 } |
37 |
37 |
38 private def print_symbol(s: Symbol.Symbol): String = |
38 private def print_symbol(s: Symbol.Symbol): String = |
39 if (s.startsWith("\\<")) s |
39 if (s.startsWith("\\<")) s |
40 else UTF8.bytes(s).iterator.map(print_byte).mkString |
40 else UTF8.bytes(s).iterator.map(print_byte).mkString |