--- a/CookBook/Parsing.thy Sat Jan 10 12:57:48 2009 +0000
+++ b/CookBook/Parsing.thy Mon Jan 12 16:03:05 2009 +0000
@@ -553,19 +553,17 @@
ML {* OuterSyntax.command *}
-section {* New Commands and Keyword Files *}
+section {* New Commands and Creating Keyword Files *}
text {*
-
Often new commands, for example for providing a new definitional principle,
- need to be programmed. While this is not too difficult to do on the
- ML-level, new commands, in order to be useful, need to be recognised by
+ need to be programmed. While this is not difficult to do 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.
-
- Let us start with a silly command, named \isacommand{foo}, which does nothing at all.
- It can be defined as
+ Let us start with a ``silly'' command, below named \isacommand{foo}, which does nothing at all.
+ On the ML-level it can be defined as
@{ML [display]
"let
@@ -575,27 +573,53 @@
OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
end"}
- The crucial function that makes the command \isacommand{foo} known to
- Isabelle is @{ML OuterSyntax.command}. It expects a name of a command, a
- short description, a flag (we will explain it later more thoroughly) and a
+ The function @{ML OuterSyntax.command} expects a name for the command, a
+ short description, a flag (which we will explain it later on more thoroughly) and a
parser for a top-level transition function (its purpose will also explained
- later on). Lets also assume we packaged this function into a separate
- theory named @{text "Command"}, say, and a file named @{text "Command.thy"}.
+ later).
- We now need a keyword file, that can be loaded by ProofGeneral in
- order to recognise \isacommand{foo} as command. Such a keyword file
- can be generated with the command-line
+ While this is everything we have to do on the ML-level, we need
+ now a keyword file that can be loaded by ProofGeneral. This is to enable ProofGeneral
+ to recognise \isacommand{foo} as a command. Such a keyword file can be generated with
+ the command-line
- @{text [display] "$ isabelle keywords -k foo some-log-files"}
+ @{text [display] "$ isabelle keywords -k foo <some-log-files>"}
The option @{text "-k foo"} indicates which postfix the keyword file will obtain. In
- the case above the generated file is named @{text "isar-keywords-foo.el"}. This command
- requires log files to be present (in order to extract the keywords from them). For
+ the case above the generated file will be named @{text "isar-keywords-foo.el"}. This command
+ requires log files to be present (in order to extract the keywords from them).
+ To generate these log files, we first package the code above into a separate theory file
+ named @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the complete code.
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{figure}[t]
+ \begin{boxedminipage}{\textwidth}
+ \isacommand{theory}~@{text Command}\\
+ \isacommand{imports}~@{text Main}\\
+ \isacommand{begin}\\
+ \isacommand{ML}~\isa{\isacharverbatimopen}\\
+ @{ML
+"let
+ val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
+ val flag = OuterKeyword.thy_decl
+in
+ OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
+end"}\\
+ \isa{\isacharverbatimclose}\\
+ \isacommand{end}
+ \end{boxedminipage}
+ \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{foo}.\label{fig:commandtheory}}
+ \end{figure}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ For
our purposes it is sufficient to use the log files for the theories @{text "Pure"},
@{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as the theory @{text "Command.thy"}
containing the new command. @{text Pure} and @{text HOL} are usually compiled during the
- installation of Isabelle, if not this can be done conveniently using build script from
- the distribution
+ installation of Isabelle. So log files for them are already available. If not, then they
+ can be conveniently compiled using build-script from the distribution
@{text [display]
"$ ./build -m \"Pure\"
@@ -605,24 +629,41 @@
@{text [display] "$ ./build -m \"Pure-ProofGeneral\" \"Pure\""}
- For the theory containing the new command \isacommand{foo}, we first
- create a ``managed'' subdirectory by
+ For the theory @{text "Command.thy"}, we first create a ``managed'' subdirectory
+ with
+
+ @{text [display] "$ isabelle mkdir FooCommand"}
+
+ This creates a directory containing the files
+
+ @{text [display]
+"./IsaMakefile
+./FooCommand/ROOT.ML
+./FooCommand/document
+./FooCommand/document/root.tex"}
- This creates files @{text "IsaMakefile"} and @{text "./FooCommand/ROOT.ML"}. We
- need to copy the file @{text "Command.thy"} into the directory @{text "FooCommand"}
- and add @{text "use_thy \"Command\";"} to @{text "./FooCommand/ROOT.ML"}.
- Now we can compile the theory by just typing
+ We need to copy the file @{text "Command.thy"} into the directory @{text "FooCommand"}
+ and add the line
+
+ @{text [display] "use_thy \"Command\";"}
+
+ to the file @{text "./FooCommand/ROOT.ML"}. Now we can compile the theory by just typing
@{text [display] "$ isabelle make"}
- All these compilations created the log files that we are after. They are typically stored
- under the directory
+ We created now the necessary log files. They are typically stored
+ in the directory
- @{text [display] "~/.isabelle/heaps/\<dots>\<dots>/\<dots>\<dots>/log"}
+ @{text [display] "~/.isabelle/heaps/Isabelle2008/polyml-5.2.1_x86-linux/log"}
- where the dots stand for names of the current Isabelle distribution and
- hardware architecture. In it are the files
+ or something similar depending on your Isabelle distribution and architecture.
+ Let us assume the name of this directory is stored in the shell variable
+ @{text "ISABELLE_LOGS"}. One way to assign this shell variable is by typing
+
+ @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
+
+ In this directory are the files
@{text [display]
"Pure.gz
@@ -630,11 +671,6 @@
Pure-ProofGeneral.gz
HOL-FooCommand.gz"}
- Let us assume the directory with these files is stored in the shell variable
- @{text "ISABELLE_LOGS"}, by typing for example
-
- @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
-
We can now create the keyword file with
@{text [display]
@@ -642,12 +678,12 @@
`$ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral,HOL-FooCommand.gz}`"}
The result is the file @{text "isar-keywords-foo.el"}, which needs to be
- copied in the directory @{text "~/.isabelle/etc"}. To make Isabelle use
- this keyword file, we need to start it with the option @{text "-k foo"}:
+ copied to the directory @{text "~/.isabelle/etc"}. To make Isabelle use
+ this keyword file, we need to start it with the option @{text "-k foo"}, i.e.
- @{text [display] "isabelle -k foo a-theory-file"}
+ @{text [display] "isabelle -k foo <a-theory-file>"}
- If we now run the original code creating the command
+ If we now run the original code
@{ML [display]
"let