equal
deleted
inserted
replaced
448 "let |
448 "let |
449 val input = filtered_input \"| in\" |
449 val input = filtered_input \"| in\" |
450 in |
450 in |
451 (OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\") input |
451 (OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\") input |
452 end" |
452 end" |
453 "((\"|\", \"in\"),[])"} |
453 "((\"|\", \"in\"), [])"} |
454 |
454 |
455 The parser @{ML "OuterParse.enum s p" for s p} parses a possibly empty |
455 The parser @{ML "OuterParse.enum s p" for s p} parses a possibly empty |
456 list of items recognised by the parser @{text p}, where the items being parsed |
456 list of items recognised by the parser @{text p}, where the items being parsed |
457 are separated by the string @{text s}. For example: |
457 are separated by the string @{text s}. For example: |
458 |
458 |
460 "let |
460 "let |
461 val input = filtered_input \"in | in | in foo\" |
461 val input = filtered_input \"in | in | in foo\" |
462 in |
462 in |
463 (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input |
463 (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input |
464 end" |
464 end" |
465 "([\"in\", \"in\", \"in\"],[\<dots>])"} |
465 "([\"in\", \"in\", \"in\"], [\<dots>])"} |
466 |
466 |
467 @{ML "OuterParse.enum1"} works similarly, except that the parsed list must |
467 @{ML "OuterParse.enum1"} works similarly, except that the parsed list must |
468 be non-empty. Note that we had to add a string @{text [quotes] "foo"} at the |
468 be non-empty. Note that we had to add a string @{text [quotes] "foo"} at the |
469 end of the parsed string, otherwise the parser would have consumed all |
469 end of the parsed string, otherwise the parser would have consumed all |
470 tokens and then failed with the exception @{text "MORE"}. Like in the |
470 tokens and then failed with the exception @{text "MORE"}. Like in the |
477 val input = filtered_input \"in | in | in\" |
477 val input = filtered_input \"in | in | in\" |
478 in |
478 in |
479 Scan.finite OuterLex.stopper |
479 Scan.finite OuterLex.stopper |
480 (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input |
480 (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input |
481 end" |
481 end" |
482 "([\"in\", \"in\", \"in\"],[])"} |
482 "([\"in\", \"in\", \"in\"], [])"} |
483 |
483 |
484 The following function will help to run examples. |
484 The following function will help to run examples. |
485 |
485 |
486 *} |
486 *} |
487 |
487 |