isabelle-cookbook: comparison CookBook/Parsing.thy

equal deleted inserted replaced

-:cd612b489504
+:02f76f1b6e7b
 "Exception FAIL raised"}
 will raise the exception @{ML_text "FAIL"}.
 There are three exceptions used in the parsing combinators:
-(FIXME: do the exception need to be explained, because the user cannot use them from ``outside''?)
 \begin{itemize}
 \item @{ML_text "FAIL"} is used to indicate that alternative routes of parsing
 might be explored.
 \item @{ML_text "MORE"} indicates that there is not enough input for the parser. For example
 in @{ML_text "($$ \"h\") []"}.
 \item @{ML_text "ABORT"} is the exception which is raised when a dead end is reached.
 It is used for example in the function @{ML "(op !!)"} (see below).
 \end{itemize}
+(FIXME: do the exception need to be explained, because the user cannot use them from ``outside''?)
 Slightly more general than the parser @{ML "(op $$)"} 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 prediate. For example the following parser either consumes an @{ML_text "h"}
+satisfying this prediate. For example the following parser either consumes an
-or a @{ML_text "w"}:
+@{ML_text [quotes] "h"} or a @{ML_text [quotes] "w"}:
 @{ML_response [display]
 "let
 val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")
 val input1 = (explode \"hello\")
 (p input1, p input2)
 end"
 "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
 The function @{ML "(op !!)"} helps to produce appropriate error messages
-during parsing. For example if one wants to parse @{ML_text p} immediately
+during parsing. For example if one wants to parse that @{ML_text p} is immediately
 followed by @{ML_text q}, or start a completely different parser @{ML_text r},
 one might write
 @{ML_open [display] "(p -- q) || r" for p q r}
 that @{ML_text p} should be followed by @{ML_text q}. To see this consider the case in
 which @{ML_text p}
 is present in the input, but not @{ML_text q}. That means @{ML_open "(p -- q)" for p q} will fail
 and the
 alternative parser @{ML_text r} will be tried. However in many circumstanes this will be the wrong
-parser for the input ``p-followed-by-q'' and therefore will fail. The error message is then caused by the
+parser for the input ``p-followed-by-q'' and therefore will also fail. The error message is then
+caused by the
 failure of @{ML_text r}, not by the absense of @{ML_text q} in the input. This kind of situation
 can be avoided by using the funtion @{ML "(op !!)"}. This function aborts the whole process of
 parsing in case of failure and invokes an error message. For example if we invoke the parser
 @{ML [display] "(!! (fn _ => \"foo\") ($$ \"h\"))"}
 This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"}
 (FIXME: give reference to later place).
 Returning to our example of parsing @{ML_open "(p -- q) || r" for p q r}. If we want
 to generate the correct error message for p-followed-by-q, then
-we have to write
+we have to write, for example
 *}
 ML {*
 fun p_followed_by_q p q r =
 let
 @{ML_response [display]
 "Scan.lift (($$ \"h\") -- ($$ \"e\")) (1,(explode \"hello\"))"
 "((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
-(FIXME: In which situations is this useful?)
+(FIXME: In which situations is this useful? Give examples.)
 *}
 section {* Parsing Theory Syntax *}
 text {*
 Most of the time, however, Isabelle developers have to deal with parsing tokens, not strings.
 This is because the parsers for the theory syntax, as well as the parsers for the
-argument syntax of proof methods and attributes, use the type
+argument syntax of proof methods and attributes use the type
 @{ML_type OuterParse.token} (which is identical to the type @{ML_type OuterLex.token}).
 \begin{readmore}
 The parser functions for the theory syntax are contained in the structure
 @{ML_struct OuterParse} defined in the file @{ML_file  "Pure/Isar/outer_parse.ML"}.
 The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}.
 \end{readmore}
 *}
-ML {* OuterLex.mk_text "hello" *}
-ML {* print_depth 50 *}
 ML {*
 let open OuterLex in
 OuterSyntax.scan Position.none "for"
 end;
 *}
-ML {* map OuterLex.mk_text (explode "hello") *}
 ML {*
 fun my_scan lex pos str =
 Source.of_string str
 |> Source.exhaust;
 *}
 ML {*
-let val toks = my_scan (["hello"], []) Position.none "hello"
+let val toks = my_scan (["hello"], []) Position.none "hello foo bar"
 in (OuterParse.$$$ "hello") toks end
-*}
-text {*
-@{ML_response_fake [display] "map OuterLex.mk_text (explode \"hello\")"
-"[Token (\<dots>), Token (\<dots>), Token (\<dots>), Token (\<dots>), Token (\<dots>)]"}
-*}
-ML {*
-OuterLex.mk_text "hello"
 *}
 ML {*
 let val input = [OuterLex.mk_text "hello", OuterLex.mk_text "world"];
 in (Scan.one (fn _ => true)) input end
 *}
+text {*
+explain @{ML "OuterParse.enum1"}, @{ML "OuterParse.prop"}
+@{ML "OuterParse.opt_target"}, @{ML "OuterParse.fixes"}
+@{ML "OuterParse.!!!"}, @{ML "OuterParse.for_fixes"}
+*}
 chapter {* Parsing *}
 text {*

changeset 43	02f76f1b6e7b
parent 42	cd612b489504
child 44	dee4b3e66dfe