760 The function @{ML_ind prop in Parse} is similar, except that it gives a different |
760 The function @{ML_ind prop in Parse} is similar, except that it gives a different |
761 error message, when parsing fails. As you can see, the parser not just returns |
761 error message, when parsing fails. As you can see, the parser not just returns |
762 the parsed string, but also some encoded information. You can decode the |
762 the parsed string, but also some encoded information. You can decode the |
763 information with the function @{ML_ind parse in YXML} in @{ML_struct YXML}. For example |
763 information with the function @{ML_ind parse in YXML} in @{ML_struct YXML}. For example |
764 |
764 |
765 @{ML_response [display,gray] |
765 @{ML_response_fake [display,gray] |
766 "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\"" |
766 "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\"" |
767 "XML.Elem (\"token\", [], [XML.Text \"foo\"])"} |
767 "Text \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""} |
768 |
768 |
769 The result of the decoding is an XML-tree. You can see better what is going on if |
769 The result of the decoding is an XML-tree. You can see better what is going on if |
770 you replace @{ML Position.none} by @{ML "Position.line 42"}, say: |
770 you replace @{ML Position.none} by @{ML "Position.line 42"}, say: |
771 |
771 |
772 @{ML_response [display,gray] |
772 @{ML_response_fake [display,gray] |
773 "let |
773 "let |
774 val input = Outer_Syntax.scan (Position.line 42) \"foo\" |
774 val input = Outer_Syntax.scan (Position.line 42) \"foo\" |
775 in |
775 in |
776 YXML.parse (fst (Parse.term input)) |
776 YXML.parse (fst (Parse.term input)) |
777 end" |
777 end" |
778 "XML.Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"} |
778 "Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"} |
779 |
779 |
780 The positional information is stored as part of an XML-tree so that code |
780 The positional information is stored as part of an XML-tree so that code |
781 called later on will be able to give more precise error messages. |
781 called later on will be able to give more precise error messages. |
782 |
782 |
783 \begin{readmore} |
783 \begin{readmore} |
784 The functions to do with input and output of XML and YXML are defined |
784 The functions to do with input and output of XML and YXML are defined |