# HG changeset patch # User Christian Urban # Date 1231776185 0 # Node ID d563f8ff6aa0b594db6b0ba2f1edad3256d90b65 # Parent c8e9a4f97916b43d419a2f234705b29259d2aec7 tuned diff -r c8e9a4f97916 -r d563f8ff6aa0 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Sat Jan 10 12:57:48 2009 +0000 +++ b/CookBook/FirstSteps.thy Mon Jan 12 16:03:05 2009 +0000 @@ -294,8 +294,9 @@ Const \ $ (Const \ $ (Free (\"P\",\) $ \)) $ (Const \ $ (Free (\"Q\",\) $ \)))"} - As can be seen, in the first case the arguments are correctly used, while in the - second the @{term "P"} and @{text "Q"} from the antiquotation. + As can be seen, in the first case the arguments are correctly used, while the + second generates a term involving the @{term "P"} and @{text "Q"} from the + antiquotation. One tricky point in constructing terms by hand is to obtain the fully qualified name for constants. For example the names for @{text "zero"} and diff -r c8e9a4f97916 -r d563f8ff6aa0 CookBook/Intro.thy --- a/CookBook/Intro.thy Sat Jan 10 12:57:48 2009 +0000 +++ b/CookBook/Intro.thy Mon Jan 12 16:03:05 2009 +0000 @@ -7,10 +7,13 @@ chapter {* Introduction *} text {* - The purpose of this Cookbook is to guide the reader through the - first steps of Isabelle programming, and to provide recipes for - solving common problems. The code provided in the Cookbook is - as far as possible checked against recent versions of Isabelle. + The purpose of this Cookbook is to guide the reader through the first steps + of Isabelle programming, and to explain some tricks of the trade. The code + provided in the Cookbook is as far as possible checked against recent + versions of Isabelle. If something does not work, then please let us + know. If you have comments or like to add to the Cookbook, you are very + welcome. + *} section {* Intended Audience and Prior Knowledge *} diff -r c8e9a4f97916 -r d563f8ff6aa0 CookBook/Parsing.thy --- 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 "} 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/\\/\\/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 "} - If we now run the original code creating the command + If we now run the original code @{ML [display] "let diff -r c8e9a4f97916 -r d563f8ff6aa0 CookBook/document/root.tex --- a/CookBook/document/root.tex Sat Jan 10 12:57:48 2009 +0000 +++ b/CookBook/document/root.tex Mon Jan 12 16:03:05 2009 +0000 @@ -11,6 +11,7 @@ \usepackage{url} \usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry} \usepackage{lineno} +\usepackage{boxedminipage} \usepackage{pdfsetup} \urlstyle{rm} diff -r c8e9a4f97916 -r d563f8ff6aa0 cookbook.pdf Binary file cookbook.pdf has changed