--- a/CookBook/Parsing.thy	Sat Feb 07 14:21:33 2009 +0000
+++ b/CookBook/Parsing.thy	Sun Feb 08 08:45:25 2009 +0000
@@ -131,7 +131,7 @@
 
   The parser @{ML "Scan.optional p x" for p x} returns the result of the parser 
   @{text "p"}, if it succeeds; otherwise it returns 
-  the default value @{text "x"}. For example
+  the default value @{text "x"}. For example:
 
 @{ML_response [display,gray]
 "let 
@@ -158,7 +158,7 @@
   The function @{ML "(op !!)"} helps to produce appropriate error messages
   during parsing. For example if you want to parse that @{text p} is immediately 
   followed by @{text q}, or start a completely different parser @{text r},
-  you might write
+  you might write:
 
   @{ML [display,gray] "(p -- q) || r" for p q r}
 
@@ -171,8 +171,8 @@
   circumstance this will be the wrong parser for the input ``p-followed-by-q''
   and therefore will also fail. The error message is then caused by the
   failure of @{text r}, not by the absence of @{text q} in the input. This
-  kind of situation can be avoided when using the function @{ML "(op
-  !!)"}. This function aborts the whole process of parsing in case of a
+  kind of situation can be avoided when using the function @{ML "(op !!)"}. 
+  This function aborts the whole process of parsing in case of a
   failure and prints an error message. For example if you invoke the parser
 
   
@@ -190,7 +190,7 @@
                                "Exception ABORT raised"}
 
   then the parsing aborts and the error message @{text "foo"} is printed out. In order to
-  see the error message, we need to prefix the parser with the function 
+  see the error message properly, we need to prefix the parser with the function 
   @{ML "Scan.error"}. For example:
 
   @{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
@@ -293,7 +293,7 @@
  ([\"f\", \"o\", \"o\"], [\"*\", \"o\", \"o\", \"o\"]))"}
 
   After parsing is done, you nearly always want to apply a function on the parsed 
-  items. To do this the function @{ML "(p >> f)" for p f} can be employed, which runs 
+  items. One way to do this is the function @{ML "(p >> f)" for p f}, which runs 
   first the parser @{text p} and upon successful completion applies the 
   function @{text f} to the result. For example
 
@@ -305,14 +305,14 @@
 end"
 "((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"}
 
-  doubles the two parsed input strings. Or
+  doubles the two parsed input strings; or
 
   @{ML_response [display,gray] 
 "let 
-   val p = Scan.repeat (Scan.one Symbol.not_eof) >> implode
+   val p = Scan.repeat (Scan.one Symbol.not_eof)
    val input = (explode \"foo bar foo\") 
 in
-   Scan.finite Symbol.stopper p input
+   Scan.finite Symbol.stopper (p >> implode) input
 end" 
 "(\"foo bar foo\",[])"}
 
@@ -344,10 +344,9 @@
 text {*
   Most of the time, however, Isabelle developers have to deal with parsing
   tokens, not strings.  This is because the parsers for the theory syntax, as
-  well as the parsers for the argument syntax of proof methods and attributes
-  use the type @{ML_type OuterLex.token} (which is identical to the type
-  @{ML_type OuterParse.token}).  There are also parsers for ML-expressions and
-  ML-files, which can be sometimes handy.
+  well as the parsers for the arguments of proof methods the type @{ML_type OuterLex.token} 
+  (which is identical to the type @{ML_type OuterParse.token}).  There are also handy 
+  parsers for ML-expressions and ML-files.
 
   \begin{readmore}
   The parser functions for the theory syntax are contained in the structure
@@ -362,8 +361,8 @@
 *}  
 
 text {*
-  With the examples below, you can generate a token list out of a string using
-  the function @{ML "OuterSyntax.scan"}, which is given @{ML "Position.none"}
+  The first example shows how to generate a token list out of a string using
+  the function @{ML "OuterSyntax.scan"}. It is given below @{ML "Position.none"}
   as argument since, at the moment, we are not interested in generating
   precise error messages. The following code
 
@@ -408,7 +407,7 @@
  Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}
 
   you obtain a list consisting of only a command and two keyword tokens.
-  If you want to see which keywords and commands are currently known, type in
+  If you want to see which keywords and commands are currently known to Isabelle, type in
   the following code (you might have to adjust the @{ML print_depth} in order to
   see the complete list):
 
@@ -500,6 +499,7 @@
   the function @{ML OuterParse.type_ident}.
   \end{exercise}
 
+  (FIXME: or give parser for numbers)
 
 *}
 
@@ -700,6 +700,7 @@
   the log file for the theory @{text "Command.thy"}, which contains the new
   \isacommand{foobar}-command. If you target other logics besides HOL, such
   as Nominal or ZF, then you need to adapt the log files appropriately.
+  
   @{text Pure} and @{text HOL} are usually compiled during the installation of
   Isabelle. So log files for them should be already available. If not, then
   they can be conveniently compiled with the help of the build-script from the Isabelle
@@ -820,7 +821,7 @@
   commands are expected to parse some arguments, for example a proposition,
   and then ``open up'' a proof in order to prove the proposition (for example
   \isacommand{lemma}) or prove some other properties (for example
-  \isacommand{function}). To achieve this kind of behaviour, we have to use the kind
+  \isacommand{function}). To achieve this kind of behaviour, you have to use the kind
   indicator @{ML thy_goal in OuterKeyword}.
 
   Below we change \isacommand{foobar} so that it takes a proposition as
@@ -875,8 +876,6 @@
   \isacommand{done}
   \end{isabelle}
 
-  Similarly for the other function composition combinators.
-
   
   (FIXME What do @{ML "Toplevel.theory"} 
   @{ML "Toplevel.print"}