--- a/CookBook/Parsing.thy	Wed Feb 25 22:13:41 2009 +0000
+++ b/CookBook/Parsing.thy	Thu Feb 26 12:16:24 2009 +0000
@@ -45,7 +45,7 @@
 
   @{ML_response [display,gray] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
 
-  This function will either succeed (as in the two examples above) or raise the exception 
+  The function @{ML "$$"} will either succeed (as in the two examples above) or raise the exception 
   @{text "FAIL"} if no string can be consumed. For example trying to parse
 
   @{ML_response_fake [display,gray] "($$ \"x\") (explode \"world\")" 
@@ -318,14 +318,6 @@
   where the single-character strings in the parsed output are transformed
   back into one string.
  
-  \begin{exercise}\label{ex:scancmts}
-  Write a parser that parses an input string so that any comment enclosed
-  inside @{text "(*\<dots>*)"} is replaced by a the same comment but enclosed inside
-  @{text "(**\<dots>**)"} in the output string. To enclose a string, you can use the
-  function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML
-  "s1 ^ s ^ s2" for s1 s2 s}.
-  \end{exercise}
-
   The function @{ML Scan.ahead} parses some input, but leaves the original
   input unchanged. For example:
 
@@ -342,6 +334,14 @@
 "((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
 
   (FIXME: In which situations is this useful? Give examples.) 
+
+  \begin{exercise}\label{ex:scancmts}
+  Write a parser that parses an input string so that any comment enclosed
+  inside @{text "(*\<dots>*)"} is replaced by a the same comment but enclosed inside
+  @{text "(**\<dots>**)"} in the output string. To enclose a string, you can use the
+  function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML
+  "s1 ^ s ^ s2" for s1 s2 s}.
+  \end{exercise}
 *}
 
 section {* Parsing Theory Syntax *}
@@ -354,7 +354,7 @@
 ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}
 
 text {*
-  This reason for using token parsers is that theory syntax, as well as the
+  The reason for using token parsers is that theory syntax, as well as the
   parsers for the arguments of proof methods, use the type @{ML_type
   OuterLex.token} (which is identical to the type @{ML_type
   OuterParse.token}).  However, there are also handy parsers for
@@ -576,7 +576,7 @@
   "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""
   "XML.Elem (\"token\", [], [XML.Text \"foo\"])"}
 
-  This function returns an XML-tree. You can see better what is going on if
+  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]
@@ -587,8 +587,8 @@
 end"
 "XML.Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"}
   
-  The positional information is stored so that code called later on will be
-  able to give more precise error messages. 
+  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. 
 
   \begin{readmore}
   The functions to do with input and output of XML and YXML are defined 
@@ -692,12 +692,12 @@
 *}
 
 text {*
-  Whenever types are given, they are stored in the @{ML SOME}s. Since types
-  are part of the inner syntax they are strings with some encoded information 
-  (see previous section). 
-  If a syntax translation is present for a variable, then it is
-  stored in the @{ML Mixfix} datastructure; no syntax translation is
-  indicated by @{ML NoSyn}.
+  Whenever types are given, they are stored in the @{ML SOME}s. They types are
+  not yet given to the variable: this must be done by type inference later
+  on. Since types are part of the inner syntax they are strings with some
+  encoded information (see previous section). If a syntax translation is
+  present for a variable, then it is stored in the @{ML Mixfix} datastructure;
+  no syntax translation is indicated by @{ML NoSyn}.
 
   \begin{readmore}
   The datastructre for sytax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
@@ -929,7 +929,9 @@
   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, you have to use the kind
-  indicator @{ML thy_goal in OuterKeyword}.
+  indicator @{ML thy_goal in OuterKeyword}.  Note, however, once you change the 
+  ``kind'' of a command from @{ML thy_decl in OuterKeyword} to @{ML thy_goal in OuterKeyword} 
+  then the keyword file needs to be re-created.
 
   Below we change \isacommand{foobar} so that it takes a proposition as
   argument and then starts a proof in order to prove it. Therefore in Line 13, 
@@ -981,8 +983,7 @@
   \isacommand{done}
   \end{isabelle}
 
-  However, once you change the ``kind'' of a command from @{ML thy_decl in OuterKeyword}
-  to @{ML thy_goal in OuterKeyword} then the keyword file needs to be re-created.
+ 
   
   (FIXME What do @{ML "Toplevel.theory"} 
   @{ML "Toplevel.print"}