isabelle-cookbook: comparison ProgTutorial/Parsing.thy

equal deleted inserted replaced

-:d111f5988e49
+:29d4701c5ee1
 val just_h = $$ \"h\" --| $$ \"e\"
 val input = Symbol.explode \"hello\"
 in
 (just_e input, just_h input)
 end"
-"((\"e\", [\"l\", \"l\", \"o\"]),(\"h\", [\"l\", \"l\", \"o\"]))"}
+"((\"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:
 @{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\""
 "[Token (\<dots>,(Keyword, \"hello\"),\<dots>),
 Token (\<dots>,(Space, \" \"),\<dots>),
 Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
-Many parsing functions later on will require spaces, comments and the like
+Many parsing functions later on will require white space, comments and the like
 to have already been filtered out.  So from now on we are going to use the
 functions @{ML filter} and @{ML OuterLex.is_proper} to do this. For example:
 @{ML_response_fake [display,gray]
 "let
 "[Token (\<dots>,(Command, \"inductive\"),\<dots>),
 Token (\<dots>,(Keyword, \"|\"),\<dots>),
 Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}
 you obtain a list consisting of only one command and two keyword tokens.
-If you want to see which keywords and commands are currently known to Isabelle, type in
+If you want to see which keywords and commands are currently known to Isabelle,
-the following code (you might have to adjust the @{ML print_depth} in order to
+type:
-see the complete list):
 @{ML_response_fake [display,gray]
 "let
 val (keywords, commands) = OuterKeyword.get_lexicons ()
 in
 (Scan.dest_lexicon commands, Scan.dest_lexicon keywords)
 end"
 "([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
+You might have to adjust the @{ML print_depth} in order to
+see the complete list.
 The parser @{ML "OuterParse.$$$"} parses a single keyword. For example:
 @{ML_response [display,gray]
 "let
 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.
-By using the parser @{ML OuterParse.position} you can decode the positional
+By using the parser @{ML OuterParse.position} you can access the token position
-information and return it as part of the parsed input. For example
+and return it as part of the parser result. For example
 @{ML_response_fake [display,gray]
 "let
-val input = (filtered_input' \"where\")
+val input = filtered_input' \"where\"
 in
 parse (OuterParse.position (OuterParse.$$$ \"where\")) input
 end"
 "((\"where\", {line=7, end_line=7}), [])"}
 OuterParse.!!!
 (OuterParse.enum1 "|"
 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
 text {*
-Note that the parser does not parse the keyword \simpleinductive, even if it is
+Note that the parser must not parse the keyword \simpleinductive, even if it is
 meant to process definitions as shown above. The parser of the keyword
 will be given by the infrastructure that will eventually call @{ML spec_parser}.
 To see what the parser returns, let us parse the string corresponding to the
 text {*
 Whenever types are given, they are stored in the @{ML SOME}s. The types are
 not yet used to type the variables: this must be done by type-inference later
 on. Since types are part of the inner syntax they are strings with some
-encoded information (see previous section). If a syntax translation is
+encoded information (see previous section). If a mixfix-syntax is
 present for a variable, then it is stored in the @{ML Mixfix} data structure;
 no syntax translation is indicated by @{ML NoSyn}.
 \begin{readmore}
-The data structure for syntax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
+The data structure for mixfix annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
 \end{readmore}
 Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a
 list of introduction rules, that is propositions with theorem annotations
 such as rule names and attributes. The introduction rules are propositions
 OuterSyntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing
 end"}\\
 @{text "\<verbclose>"}\\
 \isacommand{end}
 \end{graybox}
-\caption{The file @{text "Command.thy"} is necessary for generating a log
+\caption{This file can be used to generate a log file. This log file in turn can
-file. This log file enables Isabelle to generate a keyword file containing
+be used to generate a keyword file containing the command \isacommand{foobar}.
-the command \isacommand{foobar}.\label{fig:commandtheory}}
+\label{fig:commandtheory}}
 \end{figure}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 @{text [display] "$ isabelle make"}
 If the compilation succeeds, you have finally created all the necessary log files.
 They are stored in the directory
-@{text [display]  "~/.isabelle/heaps/Isabelle2008/polyml-5.2.1_x86-linux/log"}
+@{text [display]  "~/.isabelle/heaps/Isabelle2009/polyml-5.2.1_x86-linux/log"}
 or something similar depending on your Isabelle distribution and architecture.
 One quick way to assign a shell variable to this directory is by typing
 @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
 The result is the file @{text "isar-keywords-foobar.el"}. It should contain
 the string @{text "foobar"} twice.\footnote{To see whether things are fine, check
 that @{text "grep foobar"} on this file returns something
 non-empty.}  This keyword file needs to
-be copied into the directory @{text "~/.isabelle/etc"}. To make Isabelle
+be copied into the directory @{text "~/.isabelle/etc"}. To make ProofGeneral
 aware of this keyword file, you have to start Isabelle with the option @{text
 "-k foobar"}, that is:
 @{text [display] "$ isabelle emacs -k foobar a_theory_file"}
 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}.
 *}
 ML%linenosgray{*let
-fun prove_prop str ctxt =
+fun prove_prop str lthy =
 let
-val prop = Syntax.read_prop ctxt str
+val prop = Syntax.read_prop lthy str
 in
-Proof.theorem_i NONE (K I) [[(prop,[])]] ctxt
+Proof.theorem_i NONE (K I) [[(prop,[])]] lthy
 end;
 val prove_prop_parser = OuterParse.prop >> prove_prop
 val kind = OuterKeyword.thy_goal
 in
 \isacommand{apply}@{text "(rule conjI)"}\\
 \isacommand{apply}@{text "(rule TrueI)+"}\\
 \isacommand{done}
 \end{isabelle}
-(FIXME: read a name and show how to store theorems)
+(FIXME: read a name and show how to store theorems; see @{ML LocalTheory.note})
 *}
 section {* Methods (TBD) *}
 text {*
 \end{isabelle}
 An example of a very simple method is:
 *}
-method_setup %gray foobar_meth =
+method_setup %gray foobar =
 {* Scan.succeed
 (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *}
 "foobar method for conjE and conjI"
 text {*
-It defines the method @{text foobar_meth}, which takes no arguments (therefore the
+It defines the method @{text foobar}, which takes no arguments (therefore the
 parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which
 applies @{thm [source] conjE} and then @{thm [source] conjI}. The function @{ML SIMPLE_METHOD}
-turns such a tactic into a method. @{text "Foobar_meth"} can be used as follows
+turns such a tactic into a method. The method @{text "foobar"} can be used as follows
 *}
 lemma shows "A \<and> B \<Longrightarrow> C \<and> D"
-apply(foobar_meth)
+apply(foobar)
 txt {*
 where it results in the goal state
 \begin{minipage}{\textwidth}
 @{subgoals}

changeset 241	29d4701c5ee1
parent 240	d111f5988e49
child 244	dc95a56b1953