equal
deleted
inserted
replaced
622 |
622 |
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 pre-defined 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 OuterParse.term}. 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\" |