isabelle-cookbook: comparison CookBook/Parsing.thy

equal deleted inserted replaced

-:84d1392186d3
+:253ea99c1441
 @{ML_response [display,gray] "($$ \"h\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
 @{ML_response [display,gray] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
-This function will either succeed (as in the two examples above) or raise the exception
+The function @{ML "$$"} will either succeed (as in the two examples above) or raise the exception
 @{text "FAIL"} if no string can be consumed. For example trying to parse
 @{ML_response_fake [display,gray] "($$ \"x\") (explode \"world\")"
 "Exception FAIL raised"}
 "(\"foo bar foo\",[])"}
 where the single-character strings in the parsed output are transformed
 back into one string.
+The function @{ML Scan.ahead} parses some input, but leaves the original
+input unchanged. For example:
+@{ML_response [display,gray]
+"Scan.ahead (Scan.this_string \"foo\") (explode \"foo\")"
+"(\"foo\", [\"f\", \"o\", \"o\"])"}
+The function @{ML Scan.lift} takes a parser and a pair as arguments. This function applies
+the given parser to the second component of the pair and leaves the  first component
+untouched. For example
+@{ML_response [display,gray]
+"Scan.lift (($$ \"h\") -- ($$ \"e\")) (1,(explode \"hello\"))"
+"((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
+(FIXME: In which situations is this useful? Give examples.)
 \begin{exercise}\label{ex:scancmts}
 Write a parser that parses an input string so that any comment enclosed
 inside @{text "(*\<dots>*)"} is replaced by a the same comment but enclosed inside
 @{text "(**\<dots>**)"} in the output string. To enclose a string, you can use the
 function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML
 "s1 ^ s ^ s2" for s1 s2 s}.
 \end{exercise}
-The function @{ML Scan.ahead} parses some input, but leaves the original
-input unchanged. For example:
-@{ML_response [display,gray]
-"Scan.ahead (Scan.this_string \"foo\") (explode \"foo\")"
-"(\"foo\", [\"f\", \"o\", \"o\"])"}
-The function @{ML Scan.lift} takes a parser and a pair as arguments. This function applies
-the given parser to the second component of the pair and leaves the  first component
-untouched. For example
-@{ML_response [display,gray]
-"Scan.lift (($$ \"h\") -- ($$ \"e\")) (1,(explode \"hello\"))"
-"((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
-(FIXME: In which situations is this useful? Give examples.)
 *}
 section {* Parsing Theory Syntax *}
 text {*
 *}
 ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}
 text {*
-This reason for using token parsers is that theory syntax, as well as the
+The reason for using token parsers is that theory syntax, as well as the
 parsers for the arguments of proof methods, use the type @{ML_type
 OuterLex.token} (which is identical to the type @{ML_type
 OuterParse.token}).  However, there are also handy parsers for
 ML-expressions and ML-files.
 @{ML_response [display,gray]
 "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""
 "XML.Elem (\"token\", [], [XML.Text \"foo\"])"}
-This function returns an XML-tree. You can see better what is going on if
+The result of the decoding is an XML-tree. You can see better what is going on 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
 YXML.parse (fst (OuterParse.term input))
 end"
 "XML.Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"}
-The positional information is stored so that code called later on will be
+The positional information is stored as part of an XML-tree so that code
-able to give more precise error messages.
+called later on will be able to give more precise error messages.
 \begin{readmore}
 The functions to do with input and output of XML and YXML are defined
 in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}.
 \end{readmore}
 (bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)),
 (blonk, NONE, NoSyn)],[])"}
 *}
 text {*
-Whenever types are given, they are stored in the @{ML SOME}s. Since types
+Whenever types are given, they are stored in the @{ML SOME}s. They types are
-are part of the inner syntax they are strings with some encoded information
+not yet given to the variable: this must be done by type inference later
-(see previous section).
+on. Since types are part of the inner syntax they are strings with some
-If a syntax translation is present for a variable, then it is
+encoded information (see previous section). If a syntax translation is
-stored in the @{ML Mixfix} datastructure; no syntax translation is
+present for a variable, then it is stored in the @{ML Mixfix} datastructure;
-indicated by @{ML NoSyn}.
+no syntax translation is indicated by @{ML NoSyn}.
 \begin{readmore}
 The datastructre for sytax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
 \end{readmore}
 \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, you have to use the kind
-indicator @{ML thy_goal in OuterKeyword}.
+indicator @{ML thy_goal in OuterKeyword}.  Note, however, once you change the
+``kind'' of a command from @{ML thy_decl in OuterKeyword} to @{ML thy_goal in OuterKeyword}
+then the keyword file needs to be re-created.
 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{apply}@{text "(rule conjI)"}\\
 \isacommand{apply}@{text "(rule TrueI)+"}\\
 \isacommand{done}
 \end{isabelle}
-However, once you change the ``kind'' of a command from @{ML thy_decl in OuterKeyword}
-to @{ML thy_goal in OuterKeyword} then the keyword file needs to be re-created.
 (FIXME What do @{ML "Toplevel.theory"}
 @{ML "Toplevel.print"}
 @{ML Toplevel.local_theory} do?)

changeset 149	253ea99c1441
parent 133	3e94ccc0f31e
child 156	e8f11280c762