--- a/CookBook/Parsing.thy	Mon Oct 27 18:48:52 2008 +0100
+++ b/CookBook/Parsing.thy	Wed Oct 29 13:58:36 2008 +0100
@@ -54,8 +54,6 @@
   will raise the exception @{ML_text "FAIL"}.
   There are three exceptions used in the parsing combinators:
 
-  (FIXME: do the exception need to be explained, because the user cannot use them from ``outside''?)
-
   \begin{itemize}
   \item @{ML_text "FAIL"} is used to indicate that alternative routes of parsing 
   might be explored. 
@@ -65,11 +63,12 @@
   It is used for example in the function @{ML "(op !!)"} (see below).
   \end{itemize}
 
+  (FIXME: do the exception need to be explained, because the user cannot use them from ``outside''?)
 
   Slightly more general than the parser @{ML "(op $$)"} is the function @{ML Scan.one}, in that it 
   takes a predicate as argument and then parses exactly one item from the input list 
-  satisfying this prediate. For example the following parser either consumes an @{ML_text "h"}
-  or a @{ML_text "w"}:
+  satisfying this prediate. For example the following parser either consumes an 
+  @{ML_text [quotes] "h"} or a @{ML_text [quotes] "w"}:
 
 @{ML_response [display] 
 "let 
@@ -134,7 +133,7 @@
  "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
 
   The function @{ML "(op !!)"} helps to produce appropriate error messages
-  during parsing. For example if one wants to parse @{ML_text p} immediately 
+  during parsing. For example if one wants to parse that @{ML_text p} is immediately 
   followed by @{ML_text q}, or start a completely different parser @{ML_text r},
   one might write
 
@@ -148,7 +147,8 @@
   is present in the input, but not @{ML_text q}. That means @{ML_open "(p -- q)" for p q} will fail 
   and the 
   alternative parser @{ML_text r} will be tried. However in many circumstanes this will be the wrong
-  parser for the input ``p-followed-by-q'' and therefore will fail. The error message is then caused by the
+  parser for the input ``p-followed-by-q'' and therefore will also fail. The error message is then 
+  caused by the
   failure of @{ML_text r}, not by the absense of @{ML_text q} in the input. This kind of situation
   can be avoided by using the funtion @{ML "(op !!)"}. This function aborts the whole process of
   parsing in case of failure and invokes an error message. For example if we invoke the parser
@@ -178,7 +178,7 @@
   
   Returning to our example of parsing @{ML_open "(p -- q) || r" for p q r}. If we want
   to generate the correct error message for p-followed-by-q, then
-  we have to write
+  we have to write, for example
 *}
 
 ML {* 
@@ -239,7 +239,7 @@
 "Scan.lift (($$ \"h\") -- ($$ \"e\")) (1,(explode \"hello\"))"
 "((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
 
-  (FIXME: In which situations is this useful?) 
+  (FIXME: In which situations is this useful? Give examples.) 
 *}
 
 section {* Parsing Theory Syntax *}
@@ -247,7 +247,7 @@
 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 
+  argument syntax of proof methods and attributes use the type 
   @{ML_type OuterParse.token} (which is identical to the type @{ML_type OuterLex.token}).
 
   \begin{readmore}
@@ -257,10 +257,6 @@
   \end{readmore}
 *}
 
-ML {* OuterLex.mk_text "hello" *}
-
-ML {* print_depth 50 *}
-
 ML {* 
   let open OuterLex in 
   OuterSyntax.scan Position.none "for" 
@@ -268,8 +264,6 @@
 
 *}
 
-ML {* map OuterLex.mk_text (explode "hello") *} 
-
 ML {*
 
 fun my_scan lex pos str =
@@ -282,21 +276,10 @@
 *}
 
 ML {*
-let val toks = my_scan (["hello"], []) Position.none "hello"
+let val toks = my_scan (["hello"], []) Position.none "hello foo bar"
 in (OuterParse.$$$ "hello") toks end
 *}
 
-text {* 
-
-  @{ML_response_fake [display] "map OuterLex.mk_text (explode \"hello\")"  
-       "[Token (\<dots>), Token (\<dots>), Token (\<dots>), Token (\<dots>), Token (\<dots>)]"} 
-
-*}
-
-ML {*
-  OuterLex.mk_text "hello"
-*}
-
 ML {*
 
   let val input = [OuterLex.mk_text "hello", OuterLex.mk_text "world"];
@@ -304,7 +287,11 @@
 
 *}
 
-
+text {*
+  explain @{ML "OuterParse.enum1"}, @{ML "OuterParse.prop"} 
+   @{ML "OuterParse.opt_target"}, @{ML "OuterParse.fixes"} 
+   @{ML "OuterParse.!!!"}, @{ML "OuterParse.for_fixes"} 
+*}
 
 chapter {* Parsing *}