CookBook/Parsing.thy
changeset 60 5b9c6010897b
parent 59 b5914f3c643c
child 65 c8e9a4f97916
--- a/CookBook/Parsing.thy	Wed Dec 17 05:08:33 2008 +0000
+++ b/CookBook/Parsing.thy	Sat Jan 03 20:44:54 2009 +0000
@@ -59,7 +59,7 @@
   might be explored. 
   \item @{text "MORE"} indicates that there is not enough input for the parser. For example 
   in @{text "($$ \"h\") []"}.
-  \item @{text "ABORT"} is the exception which is raised when a dead end is reached. 
+  \item @{text "ABORT"} is the exception that is raised when a dead end is reached. 
   It is used for example in the function @{ML "(op !!)"} (see below).
   \end{itemize}
 
@@ -93,7 +93,7 @@
   Note how the result of consumed strings builds up on the left as nested pairs.  
 
   If, as in the previous example, one wants to parse a particular string, 
-  then one should rather use the function @{ML Scan.this_string}:
+  then one should use the function @{ML Scan.this_string}:
 
   @{ML_response [display] "Scan.this_string \"hel\" (explode \"hello\")"
                           "(\"hel\", [\"l\", \"o\"])"}
@@ -263,7 +263,7 @@
   end of the input string.
 
   The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can 
-  parse the input then the whole parser fails; if not, then the second is tried. Therefore
+  parse the input, then the whole parser fails; if not, then the second is tried. Therefore
   
   @{ML_response_fake_both [display] "Scan.unless ($$ \"h\") ($$ \"w\") (explode \"hello\")"
                                "Exception FAIL raised"}
@@ -277,7 +277,7 @@
 
   The functions @{ML Scan.repeat} and @{ML Scan.unless} can be combined to read any
   input until a certain marker symbol is reached. In the example below the marker
-  symbol is a @{text [quotes] "*"} which causes the parser to stop:
+  symbol is a @{text [quotes] "*"}.
 
   @{ML_response [display]
 "let 
@@ -315,7 +315,7 @@
 end" 
 "(\"foo bar foo\",[])"}
 
-  where the single strings in the parsed output are transformed
+  where the single-character strings in the parsed output are transformed
   back into one string.
  
   \begin{exercise}\label{ex:scancmts}