--- a/ProgTutorial/Parsing.thy Thu May 24 15:22:25 2012 +0100
+++ b/ProgTutorial/Parsing.thy Sat Jun 16 15:25:47 2012 +0100
@@ -935,16 +935,17 @@
*}
-section {* New Commands and Keyword Files\label{sec:newcommand} *}
+section {* New Commands\label{sec:newcommand} *}
text {*
Often new commands, for example for providing new definitional principles,
- need to be implemented. While this is not difficult on the ML-level,
- new commands, in order to be useful, need to be recognised by
- ProofGeneral. This results in some subtle configuration issues, which we
- will explain in this section.
+ need to be implemented. While this is not difficult on the ML-level and
+ jEdit, in order to be compatible, new commands need also to be recognised
+ by ProofGeneral. This results in some subtle configuration issues, which we will
+ explain in the next section. Here we just describe how to define new commands
+ to work with jEdit.
- To keep things simple, let us start with a ``silly'' command that does nothing
+ Let us start with a ``silly'' command that does nothing
at all. We shall name this command \isacommand{foobar}. On the ML-level it can be
defined as:
*}
@@ -953,19 +954,142 @@
val do_nothing = Scan.succeed (Local_Theory.background_theory I)
val kind = Keyword.thy_decl
in
- Outer_Syntax.local_theory ("foobar", kind) "description of foobar" do_nothing
+ Outer_Syntax.local_theory ("foobar", kind)
+ "description of foobar"
+ do_nothing
+end *}
+
+text {*
+ The crucial function @{ML_ind local_theory in Outer_Syntax} expects a name for the command,
+ a kind indicator (which we will explain later more thoroughly), a
+ short description and a
+ parser producing a local theory transition (its purpose will also explained
+ later). Before you can use any new command, you have to ``announce'' it in the
+ \isacommand{keyword}-section of theory header. In our running example we need
+ to write
+
+ \begin{graybox}
+ \isacommand{theory}~@{text Foo}\\
+ \isacommand{imports}~@{text Main}\\
+ \isacommand{keywords} @{text [quotes] "foobar"} @{text "::"} @{text "thy_decl"}\\
+ ...
+ \end{graybox}
+
+ whereby you have to declare again that the new keyword is of the appropriate
+ kind---for \isacommand{foobar} it is @{text "thy_decl"}. Another possible kind
+ is @{text "thy_goal"} and also to omit the kind entirely, in which case you declare a
+ keyword (something that is part of a command). After you announced the new command,
+ you can type in your theory
+*}
+
+foobar
+
+text {*
+ At the moment the command \isacommand{foobar} is not very useful. Let us
+ refine it a bit next by letting it take a proposition as argument and
+ printing this proposition inside the tracing buffer. For this the crucial
+ part of a command is the function that determines the behaviour
+ of the command. In the code above we used a ``do-nothing''-function, which
+ because of @{ML_ind succeed in Scan} does not parse any argument, but immediately
+ returns the simple function @{ML "Local_Theory.background_theory I"}. We can
+ replace this code by a function that first parses a proposition (using the
+ parser @{ML Parse.prop}), then prints out some tracing
+ information (using the function @{text trace_prop}) and
+ finally does nothing. For this you can write:
+*}
+
+ML %grayML{*let
+ fun trace_prop str =
+ Local_Theory.background_theory (fn ctxt => (tracing str; ctxt))
+
+ val kind = Keyword.thy_decl
+in
+ Outer_Syntax.local_theory ("foobar_trace", kind)
+ "traces a proposition"
+ (Parse.prop >> trace_prop)
end *}
text {*
- The crucial function @{ML_ind local_theory in Outer_Syntax} expects a name for the command, a
- short description, a kind indicator (which we will explain later more thoroughly) and a
- parser producing a local theory transition (its purpose will also explained
- later).
+ The command is now \isacommand{foobar\_trace} and can be used to
+ see the proposition in the tracing buffer (remember you need to announce
+ every new command in the header of the theory).
+*}
+
+foobar_trace "True \<and> False"
+
+text {*
+ Note that so far we used @{ML_ind thy_decl in Keyword} as the kind
+ indicator for the new command. This means that the command finishes as soon as
+ the 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, you have to use
+ the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML
+ "local_theory_to_proof" in Outer_Syntax} to set up the command.
+ Below we show the command \isacommand{foobar\_goal} which takes a
+ proposition as argument and then starts a proof in order to prove
+ it. Therefore in Line 9, we set the kind indicator to @{ML thy_goal in
+ Keyword}.
+*}
+
+ML%linenosgray{*let
+ fun goal_prop str ctxt =
+ let
+ val prop = Syntax.read_prop ctxt str
+ in
+ Proof.theorem NONE (K I) [[(prop, [])]] ctxt
+ end
+
+ val kind = Keyword.thy_goal
+in
+ Outer_Syntax.local_theory_to_proof ("foobar_goal", kind)
+ "proves a proposition"
+ (Parse.prop >> goal_prop)
+end *}
- While this is everything you have to do on the ML-level, you need a keyword
- file that can be loaded by ProofGeneral. This is to enable ProofGeneral to
- recognise \isacommand{foobar} as a command. Such a keyword file can be
- generated with the command-line:
+text {*
+ The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be
+ proved) and a context as argument. The context is necessary in order to be able to use
+ @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.
+ In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the
+ proposition. Its argument @{ML NONE} stands for a locale (which we chose to
+ omit); the argument @{ML "(K I)"} stands for a function that determines what
+ should be done with the theorem once it is proved (we chose to just forget
+ about it).
+
+ If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \<and> True"},
+ you obtain the following proof state:
+*}
+
+foobar_goal "True \<and> True"
+txt {*
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}\medskip
+
+ and can prove the proposition as follows.
+*}
+apply(rule conjI)
+apply(rule TrueI)+
+done
+
+text {*
+ While this is everything you have to do for a new command when using jEdit,
+ things are not as simple when using Emacs and ProofGeneral. We explain the details
+ next.
+*}
+
+
+section {* Proof-General and Keyword Files *}
+
+text {*
+ In order to use a new command in Emacs and Proof-General, you need a keyword
+ file that can be loaded by ProofGeneral. To keep things simple we take as
+ running example the command \isacommand{foobar} from the previous section.
+
+ A keyword file can be generated with the command-line:
@{text [display] "$ isabelle keywords -k foobar some_log_files"}
@@ -983,6 +1107,7 @@
\begin{graybox}\small
\isacommand{theory}~@{text Command}\\
\isacommand{imports}~@{text Main}\\
+ \isacommand{keywords} @{text [quotes] "foobar"} @{text "::"} @{text "thy_decl"}\\
\isacommand{begin}\\
\isacommand{ML}~@{text "\<verbopen>"}\\
@{ML
@@ -990,7 +1115,9 @@
val do_nothing = Scan.succeed (Local_Theory.background_theory I)
val kind = Keyword.thy_decl
in
- Outer_Syntax.local_theory (\"foobar\", kind) \"description of foobar\" do_nothing
+ Outer_Syntax.local_theory (\"foobar\", kind)
+ \"description of foobar\"
+ do_nothing
end"}\\
@{text "\<verbclose>"}\\
\isacommand{end}
@@ -1046,7 +1173,7 @@
If the compilation succeeds, you have finally created all the necessary log files.
They are stored in the directory
- @{text [display] "~/.isabelle/heaps/Isabelle2009/polyml-5.2.1_x86-linux/log"}
+ @{text [display] "~/.isabelle/heaps/Isabelle2012/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
@@ -1081,114 +1208,22 @@
@{text [display] "$ isabelle emacs -k foobar a_theory_file"}
If you now build a theory on top of @{text "Command.thy"},
- then you can use the command \isacommand{foobar}. You can just write
-*}
-
-foobar
+ then you can now use the command \isacommand{foobar}
+ in Proof-General
-text {*
- but you will not see any action as we chose to implement this command to do
- nothing. The point of this command is only to show the procedure of how
- to interact with ProofGeneral. A similar procedure has to be done with any
+ A similar procedure has to be done with any
other new command, and also any new keyword that is introduced with
the function @{ML_ind define in Keyword}. For example:
*}
ML %grayML{*val _ = Keyword.define ("blink", NONE) *}
-text {*
- At the moment the command \isacommand{foobar} is not very useful. Let us
- refine it a bit next by letting it take a proposition as argument and
- printing this proposition inside the tracing buffer.
-
- The crucial part of a command is the function that determines the behaviour
- of the command. In the code above we used a ``do-nothing''-function, which
- because of @{ML_ind succeed in Scan} does not parse any argument, but immediately
- returns the simple function @{ML "Local_Theory.background_theory I"}. We can
- replace this code by a function that first parses a proposition (using the
- parser @{ML Parse.prop}), then prints out the tracing
- information (using a new function @{text trace_prop}) and
- finally does nothing. For this you can write:
-*}
-
-ML %grayML{*let
- fun trace_prop str =
- Local_Theory.background_theory (fn ctxt => (tracing str; ctxt))
-
- val kind = Keyword.thy_decl
-in
- Outer_Syntax.local_theory ("foobar_trace", kind) "traces a proposition"
- (Parse.prop >> trace_prop)
-end *}
-
-text {*
- The command is now \isacommand{foobar\_trace} and can be used to
- see the proposition in the tracing buffer.
-*}
-
-foobar_trace "True \<and> False"
text {*
- Note that so far we used @{ML_ind thy_decl in Keyword} as the kind
- indicator for the command. This means that the command finishes as soon as
- the 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, you have to use
- the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML
- "local_theory_to_proof" in Outer_Syntax} to set up the command. Note,
- however, once you change the ``kind'' of a command from @{ML thy_decl in
- Keyword} to @{ML thy_goal in Keyword} then the keyword file needs
- to be re-created!
-
- Below we show the command \isacommand{foobar\_goal} which takes a
- proposition as argument and then starts a proof in order to prove
- it. Therefore in Line 9, we set the kind indicator to @{ML thy_goal in
- Keyword}.
+ Also if the kind of a command changes, from @{text "thy_decl"} to
+ @{text "thy_goal"} say, you need to recreate the keyword file.
*}
-ML%linenosgray{*let
- fun goal_prop str lthy =
- let
- val prop = Syntax.read_prop lthy str
- in
- Proof.theorem NONE (K I) [[(prop, [])]] lthy
- end
-
- val kind = Keyword.thy_goal
-in
- Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) "proves a proposition"
- (Parse.prop >> goal_prop)
-end *}
-
-text {*
- The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be
- proved) and a context as argument. The context is necessary in order to be able to use
- @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.
- In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the
- proposition. Its argument @{ML NONE} stands for a locale (which we chose to
- omit); the argument @{ML "(K I)"} stands for a function that determines what
- should be done with the theorem once it is proved (we chose to just forget
- about it). Line 9 contains the parser for the proposition.
-
- If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \<and> True"},
- you obtain the following proof state
-*}
-
-foobar_goal "True \<and> True"
-txt {*
- \begin{minipage}{\textwidth}
- @{subgoals [display]}
- \end{minipage}\medskip
-
- and can prove the proposition as follows.
-*}
-apply(rule conjI)
-apply(rule TrueI)+
-done
-
text {*
{\bf TBD below}
@@ -1197,7 +1232,7 @@
*}
ML {*
-structure Result = Proof_Data(
+structure Result = Proof_Data (
type T = unit -> term
fun init thy () = error "Result")
@@ -1398,13 +1433,15 @@
\end{minipage} *}
(*<*)oops(*>*)
-method_setup test = {* Scan.lift (Scan.succeed (K Method.succeed)) *} {* bla *}
+method_setup test = {*
+ Scan.lift (Scan.succeed (K Method.succeed)) *} {* bla *}
lemma "True"
apply(test)
oops
-method_setup joker = {* Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *}
+method_setup joker = {*
+ Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *}
lemma "False"
apply(joker)