equal
deleted
inserted
replaced
227 $$ "'" --| Scan.ahead (Scan.one (not_equal "'")); |
227 $$ "'" --| Scan.ahead (Scan.one (not_equal "'")); |
228 |
228 |
229 val scan_str = |
229 val scan_str = |
230 $$ "'" |-- $$ "'" |-- |
230 $$ "'" |-- $$ "'" |-- |
231 !! (fn (cs, _) => "Inner lexical error: malformed literal string at " ^ |
231 !! (fn (cs, _) => "Inner lexical error: malformed literal string at " ^ |
232 quote ("''" ^ beginning cs)) |
232 quote ("''" ^ Symbol.beginning cs)) |
233 (Scan.repeat scan_chr --| $$ "'" --| $$ "'"); |
233 (Scan.repeat scan_chr --| $$ "'" --| $$ "'"); |
234 |
234 |
235 |
235 |
236 fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs)); |
236 fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs)); |
237 |
237 |