556 section {* New Commands and Keyword Files *}

   556 section {* New Commands and Creating Keyword Files *}

   557 

   557 

   558 text {*

   558 text {*

   559 

   561   need to be programmed. While this is not too difficult to do on the

   560   need to be programmed. While this is not difficult to do on the ML-level,

   562   ML-level, new commands, in order to be useful, need to be recognised by

   561   new commands, in order to be useful, need to be recognised by

   566 

   565   Let us start with a ``silly'' command, below named \isacommand{foo}, which does nothing at all. 

   567   Let us start with a silly command, named \isacommand{foo}, which does nothing at all. 

   566   On the ML-level it can be defined as

   568   It can be defined as

   578   The crucial function that makes the command \isacommand{foo} known to

   576   The function @{ML OuterSyntax.command} expects a name for the command, a

   579   Isabelle is @{ML OuterSyntax.command}.  It expects a name of a command, a

   577   short description, a flag (which we will explain it later on more thoroughly) and a

   580   short description, a flag (we will explain it later more thoroughly) and a

   582   later on). Lets also assume we packaged this function into a separate

   579   later). 

   583   theory named @{text "Command"}, say, and a file named @{text "Command.thy"}. 

   580 

   584 

   581   While this is everything we have to do on the ML-level, we need 

   585   We now need a keyword file, that can be loaded by ProofGeneral in

   582   now a keyword file that can be loaded by ProofGeneral. This is to enable ProofGeneral 

   586   order to recognise \isacommand{foo} as command. Such a keyword file

   583   to recognise  \isacommand{foo} as a command. Such a keyword file can be generated with 

   587   can be generated with the command-line

   584   the command-line

   588 

   585 

   589   @{text [display] "$ isabelle keywords -k foo some-log-files"}

   586   @{text [display] "$ isabelle keywords -k foo <some-log-files>"}

   592   the case above the generated file is named @{text "isar-keywords-foo.el"}. This command

   589   the case above the generated file will be named @{text "isar-keywords-foo.el"}. This command

   593   requires log files to be present (in order to extract the keywords from them). For 

   590   requires log files to be present (in order to extract the keywords from them). 

   591   To generate these log files, we first package the code above into a separate theory file 

   592   named @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the complete code. 

   593 

   594   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   595   \begin{figure}[t]

   596   \begin{boxedminipage}{\textwidth}

   597   \isacommand{theory}~@{text Command}\\

   598   \isacommand{imports}~@{text Main}\\

   599   \isacommand{begin}\\

   600   \isacommand{ML}~\isa{\isacharverbatimopen}\\

   601   @{ML

   602 "let

   603   val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))

   604   val flag = OuterKeyword.thy_decl

   605 in

   606   OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing

   607 end"}\\

   608   \isa{\isacharverbatimclose}\\

   609   \isacommand{end}

   610   \end{boxedminipage}

   611   \caption{The file @{text "Command.thy"} is necessary for generating a log 

   612   file. This log file enables Isabelle to generate a keyword file containing 

   613   the command \isacommand{foo}.\label{fig:commandtheory}}

   614   \end{figure}

   615   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   616 

   617   For 

   597   installation of Isabelle, if not this can be done conveniently using build script from 

   621   installation of Isabelle. So log files for them are already available. If not, then they 

   598   the distribution

   622   can be conveniently compiled using build-script from the distribution

   608   For the theory containing the new command \isacommand{foo}, we first

   632   For the theory @{text "Command.thy"}, we first create a ``managed'' subdirectory 

   609   create a ``managed'' subdirectory by

   633   with

   610 

   634 

   611 

   635   @{text [display] "$ isabelle mkdir FooCommand"}

   612   This creates files @{text "IsaMakefile"} and @{text "./FooCommand/ROOT.ML"}. We

   636 

   613   need to copy the file @{text "Command.thy"} into the directory @{text "FooCommand"}

   637   This creates a directory containing the files 

   614   and add @{text "use_thy \"Command\";"} to @{text "./FooCommand/ROOT.ML"}.

   638 

   615   Now we can compile the theory by just typing

   639   @{text [display] 

   640 "./IsaMakefile

   641 ./FooCommand/ROOT.ML

   642 ./FooCommand/document

   643 ./FooCommand/document/root.tex"}

   644 

   645 

   646   We need to copy the file @{text "Command.thy"} into the directory @{text "FooCommand"}

   647   and add the line 

   648 

   649   @{text [display] "use_thy \"Command\";"} 

   650   

   651   to the file @{text "./FooCommand/ROOT.ML"}. Now we can compile the theory by just typing

   619   All these compilations created the log files that we are after. They are typically stored 

   655   We created now the necessary log files. They are typically stored 

   620   under the directory 

   656   in the directory 

   621   

   657   

   622   @{text [display]  "~/.isabelle/heaps/\<dots>\<dots>/\<dots>\<dots>/log"}

   658   @{text [display]  "~/.isabelle/heaps/Isabelle2008/polyml-5.2.1_x86-linux/log"}

   623 

   659 

   624   where the dots stand for names of the current Isabelle distribution and 

   660   or something similar depending on your Isabelle distribution and architecture. 

   625   hardware architecture. In it are the files

   661   Let us assume the name of this directory is stored in the shell variable 

   662   @{text "ISABELLE_LOGS"}. One way to assign this shell variable is by typing

   663 

   664   @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}

   665  

   666   In this directory are the files

   645   copied in the directory @{text "~/.isabelle/etc"}. To make Isabelle use

   681   copied to the directory @{text "~/.isabelle/etc"}. To make Isabelle use

   646   this keyword file, we need to start it with the option @{text "-k foo"}:

   682   this keyword file, we need to start it with the option @{text "-k foo"}, i.e.

   647 

   683 

   648   @{text [display] "isabelle -k foo a-theory-file"}

   684   @{text [display] "isabelle -k foo <a-theory-file>"}

   649 

   685 

   650   If we now run the original code creating the command

   686   If we now run the original code