diff -r b5914f3c643c -r 5b9c6010897b CookBook/Parsing.thy --- 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}