--- a/ProgTutorial/Parsing.thy Sat Apr 25 14:28:58 2009 +0200
+++ b/ProgTutorial/Parsing.thy Sat Apr 25 17:46:47 2009 +0200
@@ -146,7 +146,7 @@
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
@@ -424,7 +424,7 @@
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:
@@ -452,9 +452,8 @@
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
- the following code (you might have to adjust the @{ML print_depth} in order to
- see the complete list):
+ If you want to see which keywords and commands are currently known to Isabelle,
+ type:
@{ML_response_fake [display,gray]
"let
@@ -464,6 +463,9 @@
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]
@@ -579,12 +581,12 @@
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
- information and return it as part of the parsed input. For example
+ By using the parser @{ML OuterParse.position} you can access the token position
+ 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"
@@ -683,7 +685,7 @@
(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}.
@@ -734,12 +736,12 @@
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
@@ -858,9 +860,9 @@
@{text "\<verbclose>"}\\
\isacommand{end}
\end{graybox}
- \caption{The file @{text "Command.thy"} is necessary for generating a log
- file. This log file enables Isabelle to generate a keyword file containing
- the command \isacommand{foobar}.\label{fig:commandtheory}}
+ \caption{This file can be used to generate a log file. This log file in turn can
+ be used to generate a keyword file containing the command \isacommand{foobar}.
+ \label{fig:commandtheory}}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -909,7 +911,7 @@
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
@@ -937,7 +939,7 @@
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:
@@ -1010,11 +1012,11 @@
*}
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
@@ -1052,7 +1054,8 @@
\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) *}
@@ -1075,20 +1078,20 @@
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