# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1281693930 -28800
# Node ID 2f39df9ceb6328696e598a18294668a8e9c6486a
# Parent  ec45ab852586fcdb3825530288fa5ff227ec6f27
updated to new isabelle

diff -r ec45ab852586 -r 2f39df9ceb63 ProgTutorial/Parsing.thy
--- 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. 
 
diff -r ec45ab852586 -r 2f39df9ceb63 progtutorial.pdf
Binary file progtutorial.pdf has changed