isabelle-cookbook: comparison CookBook/Parsing.thy

equal deleted inserted replaced

-:258ce361ba1b
+:8bea3f74889d
 section {* Building Generic Parsers *}
 text {*
 Let us first have a look at parsing strings using generic parsing combinators.
-The function @{ML "(op $$)"} takes a string as argument and will ``consume'' this string from
+The function @{ML "$$"} takes a string as argument and will ``consume'' this string from
 a given input list of strings. ``Consume'' in this context means that it will
 return a pair consisting of this string and the rest of the input list.
 For example:
 @{ML_response [display,gray] "($$ \"h\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
 \item @{text "FAIL"} is used to indicate that alternative routes of parsing
 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 that is raised when a dead end is reached.
-It is used for example in the function @{ML "(op !!)"} (see below).
+It is used for example in the function @{ML "!!"} (see below).
 \end{itemize}
 However, note that these exceptions are private to the parser and cannot be accessed
 by the programmer (for example to handle them).
-Slightly more general than the parser @{ML "(op $$)"} is the function @{ML
+Slightly more general than the parser @{ML "$$"} 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 predicate. For example the
 following parser either consumes an @{text [quotes] "h"} or a @{text
 [quotes] "w"}:
 in
 (hw input1, hw input2)
 end"
 "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
-Two parser can be connected in sequence by using the function @{ML "(op --)"}.
+Two parser can be connected in sequence by using the function @{ML "--"}.
 For example parsing @{text "h"}, @{text "e"} and @{text "l"} in this
 sequence you can achieve by:
 @{ML_response [display,gray] "(($$ \"h\") -- ($$ \"e\") -- ($$ \"l\")) (explode \"hello\")"
 "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
 @{ML_response [display,gray] "Scan.this_string \"hell\" (explode \"hello\")"
 "(\"hell\", [\"o\"])"}
 Parsers that explore alternatives can be constructed using the function @{ML
-"(op ||)"}. For example, the parser @{ML "(p || q)" for p q} returns the
+"||"}. For example, the parser @{ML "(p || q)" for p q} returns the
 result of @{text "p"}, in case it succeeds, otherwise it returns the
 result of @{text "q"}. For example:
 @{ML_response [display,gray]
 in
 (hw input1, hw input2)
 end"
 "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
-The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing function
+The functions @{ML "|--"} and @{ML "--|"} work like the sequencing function
 for parsers, except that they discard the item being parsed by the first (respectively second)
 parser. For example:
 @{ML_response [display,gray]
 "let
 val input2 = (explode \"world\")
 in
 (p input1, p input2)
 end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
-The function @{ML "(op !!)"} helps to produce appropriate error messages
+The function @{ML "!!"} helps to produce appropriate error messages
 during parsing. For example if you want to parse that @{text p} is immediately
 followed by @{text q}, or start a completely different parser @{text r},
 you might write:
 @{ML [display,gray] "(p -- q) || r" for p q r}
 the input, but not @{text q}. That means @{ML "(p -- q)" for p q} will fail
 and the alternative parser @{text r} will be tried. However in many
 circumstance this will be the wrong parser for the input ``p-followed-by-q''
 and therefore will also fail. The error message is then caused by the
 failure of @{text r}, not by the absence of @{text q} in the input. This
-kind of situation can be avoided when using the function @{ML "(op !!)"}.
+kind of situation can be avoided when using the function @{ML "!!"}.
 This function aborts the whole process of parsing in case of a
 failure and prints an error message. For example if you invoke the parser
 @{ML [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\"))"}
 but if you invoke it on @{text [quotes] "world"}
 @{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")"
 "Exception ABORT raised"}
-then the parsing aborts and the error message @{text "foo"} is printed out. In order to
+then the parsing aborts and the error message @{text "foo"} is printed. In order to
 see the error message properly, we need to prefix the parser with the function
 @{ML "Scan.error"}. For example:
 @{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
 "Exception Error \"foo\" raised"}
 in
 (OuterParse.$$$ \"where\" input1, OuterParse.$$$ \"|\" input2)
 end"
 "((\"where\",\<dots>),(\"|\",\<dots>))"}
-Like before, you can sequentially connect parsers with @{ML "(op --)"}. For example:
+Like before, you can sequentially connect parsers with @{ML "--"}. For example:
 @{ML_response [display,gray]
 "let
 val input = filtered_input \"| in\"
 in
 indicated by @{ML NoSyn}.
 (FIXME: should for-fixes take any syntax annotation?)
 @{ML OuterParse.for_fixes} is an ``optional'' that prefixes
-@{ML OuterParse.fixes} with the comman \isacommand{for}.
+@{ML OuterParse.fixes} with the command \isacommand{for}.
 (FIXME give an example and explain more)
 @{ML_response [display,gray]
 "let
 val input = filtered_input

changeset 108	8bea3f74889d
parent 105	f49dc7e96235
child 114	13fd0a83d3c3