CookBook/Parsing.thy
changeset 183 8bb4eaa2ec92
parent 181 5baaabe1ab92
child 186 371e4375c994
--- 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.