--- a/ProgTutorial/Parsing.thy	Wed Jul 28 20:59:57 2010 +0100
+++ b/ProgTutorial/Parsing.thy	Fri Aug 13 18:05:30 2010 +0800
@@ -762,21 +762,21 @@
   the parsed string, but also some encoded information. You can decode the
   information with the function @{ML_ind parse in YXML} in @{ML_struct YXML}. For example
 
-  @{ML_response [display,gray]
+  @{ML_response_fake [display,gray]
   "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""
-  "XML.Elem (\"token\", [], [XML.Text \"foo\"])"}
+  "Text \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""}
 
   The result of the decoding is an XML-tree. You can see better what is going on if
   you replace @{ML Position.none} by @{ML "Position.line 42"}, say:
 
-@{ML_response [display,gray]
+@{ML_response_fake [display,gray]
 "let 
   val input = Outer_Syntax.scan (Position.line 42) \"foo\"
 in 
   YXML.parse (fst (Parse.term input))
 end"
-"XML.Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"}
-  
+"Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"}
+
   The positional information is stored as part of an XML-tree so that code 
   called later on will be able to give more precise error messages. 
 

Binary file progtutorial.pdf has changed