ProgTutorial/Parsing.thy
changeset 445 2f39df9ceb63
parent 426 d94755882e36
child 449 f952f2679a11
equal deleted inserted replaced
444:ec45ab852586 445:2f39df9ceb63
   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