equal
deleted
inserted
replaced
430 |
430 |
431 fun is_plain s = is_ascii s andalso s <> "\^M" andalso s <> "\\"; |
431 fun is_plain s = is_ascii s andalso s <> "\^M" andalso s <> "\\"; |
432 |
432 |
433 fun is_utf8_trailer s = is_char s andalso 128 <= ord s andalso ord s < 192; |
433 fun is_utf8_trailer s = is_char s andalso 128 <= ord s andalso ord s < 192; |
434 |
434 |
|
435 fun implode_pseudo_utf8 (cs as ["\192", c]) = |
|
436 if ord c < 160 then chr (ord c - 128) else implode cs |
|
437 | implode_pseudo_utf8 cs = implode cs; |
|
438 |
435 val scan_encoded_newline = |
439 val scan_encoded_newline = |
436 $$ "\^M" -- $$ "\n" >> K "\n" || |
440 $$ "\^M" -- $$ "\n" >> K "\n" || |
437 $$ "\^M" >> K "\n" || |
441 $$ "\^M" >> K "\n" || |
438 Scan.this_string "\\<^newline>" >> K "\n"; |
442 Scan.this_string "\\<^newline>" >> K "\n"; |
439 |
443 |
441 Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) || |
445 Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) || |
442 Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode); |
446 Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode); |
443 |
447 |
444 val scan = |
448 val scan = |
445 Scan.one is_plain || |
449 Scan.one is_plain || |
446 Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode || |
450 Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode_pseudo_utf8 || |
447 scan_encoded_newline || |
451 scan_encoded_newline || |
448 ($$ "\\" ^^ $$ "<" ^^ |
452 ($$ "\\" ^^ $$ "<" ^^ |
449 !! (fn (cs, _) => malformed_msg (beginning 10 ("\\" :: "<" :: cs))) |
453 !! (fn (cs, _) => malformed_msg (beginning 10 ("\\" :: "<" :: cs))) |
450 (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) || |
454 (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) || |
451 Scan.one not_eof; |
455 Scan.one not_eof; |