--- 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}