623 section {* Parsing Inner Syntax *} |
623 section {* Parsing Inner Syntax *} |
624 |
624 |
625 text {* |
625 text {* |
626 There is usually no need to write your own parser for parsing inner syntax, that is |
626 There is usually no need to write your own parser for parsing inner syntax, that is |
627 for terms and types: you can just call the predefined parsers. Terms can |
627 for terms and types: you can just call the predefined parsers. Terms can |
628 be parsed using the function @{ML OuterParse.term}. For example: |
628 be parsed using the function @{ML [index] term in OuterParse}. For example: |
629 |
629 |
630 @{ML_response [display,gray] |
630 @{ML_response [display,gray] |
631 "let |
631 "let |
632 val input = OuterSyntax.scan Position.none \"foo\" |
632 val input = OuterSyntax.scan Position.none \"foo\" |
633 in |
633 in |
634 OuterParse.term input |
634 OuterParse.term input |
635 end" |
635 end" |
636 "(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"} |
636 "(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"} |
637 |
637 |
638 The function @{ML OuterParse.prop} is similar, except that it gives a different |
638 The function @{ML [index] prop in OuterParse} is similar, except that it gives a different |
639 error message, when parsing fails. As you can see, the parser not just returns |
639 error message, when parsing fails. As you can see, the parser not just returns |
640 the parsed string, but also some encoded information. You can decode the |
640 the parsed string, but also some encoded information. You can decode the |
641 information with the function @{ML YXML.parse}. For example |
641 information with the function @{ML [index] parse in YXML}. For example |
642 |
642 |
643 @{ML_response [display,gray] |
643 @{ML_response [display,gray] |
644 "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\"" |
644 "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\"" |
645 "XML.Elem (\"token\", [], [XML.Text \"foo\"])"} |
645 "XML.Elem (\"token\", [], [XML.Text \"foo\"])"} |
646 |
646 |