isabelle-cookbook: comparison CookBook/Parsing.thy

equal deleted inserted replaced

-:fe10da5354a3
+:5dcad9348e4d
 end"
 "((\"e\", [\"l\", \"l\", \"o\"]),(\"h\", [\"l\", \"l\", \"o\"]))"}
 The parser @{ML "Scan.optional p x" for p x} returns the result of the parser
 @{text "p"}, if it succeeds; otherwise it returns
-the default value @{text "x"}. For example
+the default value @{text "x"}. For example:
 @{ML_response [display,gray]
 "let
 val p = Scan.optional ($$ \"h\") \"x\"
 val input1 = (explode \"hello\")
 end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
 The function @{ML "(op !!)"} 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
+you might write:
 @{ML [display,gray] "(p -- q) || r" for p q r}
 However, this parser is problematic for producing an appropriate error
 message, in case the parsing of @{ML "(p -- q)" for p q} fails. Because in
 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 "(op !!)"}.
-!!)"}. This function aborts the whole process of parsing in case of a
+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\"))"}
 @{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
-see the error message, we need to prefix the parser with the function
+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"}
 end"
 "(([\"f\", \"o\", \"o\", \"o\", \"o\", \"o\"], []),
 ([\"f\", \"o\", \"o\"], [\"*\", \"o\", \"o\", \"o\"]))"}
 After parsing is done, you nearly always want to apply a function on the parsed
-items. To do this the function @{ML "(p >> f)" for p f} can be employed, which runs
+items. One way to do this is the function @{ML "(p >> f)" for p f}, which runs
 first the parser @{text p} and upon successful completion applies the
 function @{text f} to the result. For example
 @{ML_response [display,gray]
 "let
 in
 (($$ \"h\") -- ($$ \"e\") >> double) (explode \"hello\")
 end"
 "((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"}
-doubles the two parsed input strings. Or
+doubles the two parsed input strings; or
 @{ML_response [display,gray]
 "let
-val p = Scan.repeat (Scan.one Symbol.not_eof) >> implode
+val p = Scan.repeat (Scan.one Symbol.not_eof)
 val input = (explode \"foo bar foo\")
 in
-Scan.finite Symbol.stopper p input
+Scan.finite Symbol.stopper (p >> implode) input
 end"
 "(\"foo bar foo\",[])"}
 where the single-character strings in the parsed output are transformed
 back into one string.
 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
+well as the parsers for the arguments of proof methods the type @{ML_type OuterLex.token}
-use the type @{ML_type OuterLex.token} (which is identical to the type
+(which is identical to the type @{ML_type OuterParse.token}).  There are also handy
-@{ML_type OuterParse.token}).  There are also parsers for ML-expressions and
+parsers for ML-expressions and ML-files.
-ML-files, which can be sometimes handy.
 \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"}.
 @{ML "Command" in OuterLex} for commands). Some token parsers take into account the
 kind of tokens.
 *}
 text {*
-With the examples below, you can generate a token list out of a string using
+The first example shows how to generate a token list out of a string using
-the function @{ML "OuterSyntax.scan"}, which is given @{ML "Position.none"}
+the function @{ML "OuterSyntax.scan"}. It is given below @{ML "Position.none"}
 as argument since, at the moment, we are not interested in generating
 precise error messages. The following code
 @{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\""
 "[Token (\<dots>,(Ident, \"hello\"),\<dots>),
 "[Token (\<dots>,(Command, \"inductive\"),\<dots>),
 Token (\<dots>,(Keyword, \"|\"),\<dots>),
 Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}
 you obtain a list consisting of only a command and two keyword tokens.
-If you want to see which keywords and commands are currently known, type in
+If you want to see which keywords and commands are currently known to Isabelle, type in
 the following code (you might have to adjust the @{ML print_depth} in order to
 see the complete list):
 @{ML_response_fake [display,gray]
 "let
 A type-identifier, for example @{typ "'a"}, is a token of
 kind @{ML "Keyword" in OuterLex}. It can be parsed using
 the function @{ML OuterParse.type_ident}.
 \end{exercise}
+(FIXME: or give parser for numbers)
 *}
 For our purposes it is sufficient to use the log files of the theories
 @{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as
 the log file for the theory @{text "Command.thy"}, which contains the new
 \isacommand{foobar}-command. If you target other logics besides HOL, such
 as Nominal or ZF, then you need to adapt the log files appropriately.
 @{text Pure} and @{text HOL} are usually compiled during the installation of
 Isabelle. So log files for them should be already available. If not, then
 they can be conveniently compiled with the help of the build-script from the Isabelle
 distribution.
 arguments are processed. Examples of this kind of commands are
 \isacommand{definition} and \isacommand{declare}.  In other cases,
 commands are expected to parse some arguments, for example a proposition,
 and then ``open up'' a proof in order to prove the proposition (for example
 \isacommand{lemma}) or prove some other properties (for example
-\isacommand{function}). To achieve this kind of behaviour, we have to use the kind
+\isacommand{function}). To achieve this kind of behaviour, you have to use the kind
 indicator @{ML thy_goal in OuterKeyword}.
 Below we change \isacommand{foobar} so that it takes a proposition as
 argument and then starts a proof in order to prove it. Therefore in Line 13,
 we set the kind indicator to @{ML thy_goal in OuterKeyword}.
 \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
 \isacommand{apply}@{text "(rule conjI)"}\\
 \isacommand{apply}@{text "(rule TrueI)+"}\\
 \isacommand{done}
 \end{isabelle}
-Similarly for the other function composition combinators.
 (FIXME What do @{ML "Toplevel.theory"}
 @{ML "Toplevel.print"}
 @{ML Toplevel.local_theory}?)

changeset 104	5dcad9348e4d
parent 102	5e309df58557
child 105	f49dc7e96235