isabelle-cookbook: comparison CookBook/Parsing.thy

equal deleted inserted replaced

-:748d9c1a32fb
+:fcc0e6e54dca
 Token ((\"bar\", ({line=8, end_line=8}, {line=8})), (Ident, \"bar\"), \<dots>)]"}
 in which the @{text [quotes] "\\n"} causes the second token to be in
 line 8.
-Now by using the parser @{ML OuterParse.position} you can decode the positional
+By using the parser @{ML OuterParse.position} you can decode the positional
 information and return it as part of the parsed input. For example
 @{ML_response_fake [display,gray]
 "let
 val input = (filtered_input' \"where\")
 "(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"}
 The function @{ML OuterParse.prop} is similar, except that it gives a different
 error message, when parsing fails. Looking closer at the result string you will
 have noticed that the parser not just returns the parsed string, but also some
-encoded positional information. You can see this better if you replace
+encoded information. You can see this better if you replace
 @{ML Position.none} by @{ML "(Position.line 42)"}, say.
 @{ML_response [display,gray]
 "let
 val input = OuterSyntax.scan (Position.line 42) \"foo\"
 in
 OuterParse.term input
 end"
 "(\"\\^E\\^Ftoken\\^Fline=42\\^Fend_line=42\\^Efoo\\^E\\^F\\^E\", [])"}
-The positional information is stored so that code called later will be
+The positional information is stored so that code called later on will be
 able to give more precise error messages.
 *}
 section {* Parsing Specifications\label{sec:parsingspecs} *}
 text {*
 For this we are going to use the parser:
 *}
 ML %linenosgray{*val spec_parser =
 OuterParse.opt_target --
 OuterParse.fixes --
 OuterParse.for_fixes --
 Scan.optional
 (OuterParse.$$$ "where" |--
 OuterParse.!!!
 (OuterParse.enum1 "|"
 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
 text {*
-Note that the parser does not parse the ketword \simpleinductive. This
+Note that the parser does not parse the keyword \simpleinductive, even if it is
-will be done by the infrastructure that will eventually call this parser.
+meant to process definitions as shown above. The parser of the keyword
+will be given by the infrastructure that will eventually calls @{ML spec_parser}.
 To see what the parser returns, let us parse the string corresponding to the
 definition of @{term even} and @{term odd}:
 @{ML_response [display,gray]
 "let
 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
 As can be seen, the result is a ``nested'' four-tuple consisting of an
-optional locale; a list of variables with optional type-annotation and
+optional locale (in this case @{ML NONE}); a list of variables with optional
-syntax-annotation; a list of for-fixes (fixed variables); and a list of rules
+type-annotation and syntax-annotation; a list of for-fixes (fixed variables; in this
-where each rule has optionally a name and an attribute.
+case there are none); and a list of rules where every rule has optionally a name and
+an attribute.
 In Line 2 of the parser, the function @{ML OuterParse.opt_target} reads a target
 in order to indicate a locale in which the specification is made. For example
 @{ML_response [display,gray]
 "parse OuterParse.opt_target (filtered_input \"(in test)\")" "(SOME \"test\",[])"}
-returns the locale @{text [quotes] "test"}; if no target is given' like in  the
+returns the locale @{text [quotes] "test"}; if no target is given, like in  the
-casde of @{text "even"} and @{text "odd"}, the function returns @{ML NONE}.
+case of @{text "even"} and @{text "odd"}, the function returns @{ML NONE}.
 The function @{ML OuterParse.fixes} in Line 3 reads an \isacommand{and}-separated
 list of variables that can include optional type annotations and syntax translations.
 For example:\footnote{Note that in the code we need to write
 @{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes
 (blonk, NONE, NoSyn)],[])"}
 *}
 text {*
 Whenever types are given, they are stored in the @{ML SOME}s. Since types
-are part of the inner syntax they are strings with some printing directives
+are part of the inner syntax they are strings with some encoded information
 (see previous section).
 If a syntax translation is present for a variable, then it is
 stored in the @{ML Mixfix} datastructure; no syntax translation is
 indicated by @{ML NoSyn}.
 val ((name, attrib), _) = parse (SpecParse.thm_name \":\") input
 in
 (name, map Args.dest_src attrib)
 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
-A name of a theorem can be quite complicated, as it can include attrinutes.
 The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
 @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some
 attributes. If you want to print out all currently known attributes a theorem
 can have, you can use the function:
 HOL.dest:  declaration of Classical destruction rule
 HOL.elim:  declaration of Classical elimination rule
 \<dots>"}
-For the inductive definitions described above only, the attibutes @{text "[intro]"} and
+For the inductive definitions described above only the attibutes @{text "[intro]"} and
 @{text "[simp]"} make sense.
 \begin{readmore}
 Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"}
 and @{ML_file "Pure/Isar/args.ML"}.

changeset 126	fcc0e6e54dca
parent 125	748d9c1a32fb
child 127	74846cb0fff9