equal
deleted
inserted
replaced
38 (!! (fn _ => "Expected to find an identifier in " ^ s) |
38 (!! (fn _ => "Expected to find an identifier in " ^ s) |
39 (Scan.any Symbol.is_blank |-- Syntax.scan_id))) |
39 (Scan.any Symbol.is_blank |-- Syntax.scan_id))) |
40 |> #1; |
40 |> #1; |
41 |
41 |
42 fun is_backslash c = c = "\\"; |
42 fun is_backslash c = c = "\\"; |
43 |
|
44 (*Apply string escapes to a quoted string; see Def of Standard ML, page 3 |
|
45 Does not handle the \ddd form; no error checking*) |
|
46 fun escape [] = [] |
|
47 | escape cs = (case take_prefix (not o is_backslash) cs of |
|
48 (front, []) => front |
|
49 | (front, _::"n"::rest) => front @ ("\n" :: escape rest) |
|
50 | (front, _::"t"::rest) => front @ ("\t" :: escape rest) |
|
51 | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest) |
|
52 | (front, _::"\""::rest) => front @ ("\"" :: escape rest) |
|
53 | (front, _::"\\"::rest) => front @ ("\\" :: escape rest) |
|
54 | (front, b::c::rest) => |
|
55 if Symbol.is_blank c (*remove any further blanks and the following \ *) |
|
56 then front @ escape (tl (snd (take_prefix Symbol.is_blank rest))) |
|
57 else error ("Unrecognized string escape: " ^ implode(b::c::rest))); |
|
58 |
|
59 (*Remove the first and last charaters -- presumed to be quotes*) |
|
60 val trim = implode o escape o rev o tl o rev o tl o Symbol.explode; |
|