--- a/CookBook/Parsing.thy Tue Mar 17 12:26:34 2009 +0100
+++ b/CookBook/Parsing.thy Tue Mar 17 17:32:12 2009 +0100
@@ -450,7 +450,7 @@
in
(OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\") input
end"
-"((\"|\", \"in\"),[])"}
+"((\"|\", \"in\"), [])"}
The parser @{ML "OuterParse.enum s p" for s p} parses a possibly empty
list of items recognised by the parser @{text p}, where the items being parsed
@@ -462,7 +462,7 @@
in
(OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
end"
-"([\"in\", \"in\", \"in\"],[\<dots>])"}
+"([\"in\", \"in\", \"in\"], [\<dots>])"}
@{ML "OuterParse.enum1"} works similarly, except that the parsed list must
be non-empty. Note that we had to add a string @{text [quotes] "foo"} at the
@@ -479,7 +479,7 @@
Scan.finite OuterLex.stopper
(OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
end"
-"([\"in\", \"in\", \"in\"],[])"}
+"([\"in\", \"in\", \"in\"], [])"}
The following function will help to run examples.