582 

   582 

   583   @{text [display] "$ isabelle keywords -k foobar some_log_files"}

   583   @{text [display] "$ isabelle keywords -k foobar some_log_files"}

   584 

   584 

   585   The option @{text "-k foobar"} indicates which postfix the name of the keyword file 

   585   The option @{text "-k foobar"} indicates which postfix the name of the keyword file 

   586   will be assigned. In the case above the file will be named @{text

   586   will be assigned. In the case above the file will be named @{text

   588   present (in order to extract the keywords from them). To generate these log

   588   present (in order to extract the keywords from them). To generate these log

   589   files, we first package the code above into a separate theory file named

   589   files, we first package the code above into a separate theory file named

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

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

   591   complete code.

   591   complete code.

   592 

   592 

   681 @{text [display]

   681 @{text [display]

   682 "$ isabelle keywords -k foobar 

   682 "$ isabelle keywords -k foobar 

   683    $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}

   683    $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}

   684 

   684 

   685   The result is the file @{text "isar-keywords-foobar.el"}. It should contain

   685   The result is the file @{text "isar-keywords-foobar.el"}. It should contain

   687   that @{text "grep foobar"} on this file returns something

   687   that @{text "grep foobar"} on this file returns something

   689   be copied into the directory @{text "~/.isabelle/etc"}. To make Isabelle

   689   be copied into the directory @{text "~/.isabelle/etc"}. To make Isabelle

   690   aware of this keyword file, we have to start Isabelle with the option @{text

   690   aware of this keyword file, we have to start Isabelle with the option @{text

   691   "-k foobar"}, i.e.

   691   "-k foobar"}, i.e.

   692 

   692 

   693 

   693 

   738   for the command.  This means that the command finishes as soon as the

   738   for the command.  This means that the command finishes as soon as the

   739   arguments are processed. Examples of this kind of commands are

   739   arguments are processed. Examples of this kind of commands are

   740   \isacommand{definition} and \isacommand{declare}.  In other cases,

   740   \isacommand{definition} and \isacommand{declare}.  In other cases,

   741   commands are expected to parse some arguments, for example a proposition,

   741   commands are expected to parse some arguments, for example a proposition,

   742   and then ``open up'' a proof in order to prove the proposition (for example

   742   and then ``open up'' a proof in order to prove the proposition (for example

   744   \isacommand{function}). To achieve this kind of behaviour, we have to use the kind

   744   \isacommand{function}). To achieve this kind of behaviour, we have to use the kind

   745   indicator @{ML thy_goal in OuterKeyword}.

   745   indicator @{ML thy_goal in OuterKeyword}.

   746 

   746 

   747   Below we change \isacommand{foobar} so that it takes a proposition as

   747   Below we change \isacommand{foobar} so that it takes a proposition as

   748   argument and then starts a proof in order to prove it. Therefore in Line 13

   748   argument and then starts a proof in order to prove it. Therefore in Line 13

   765 in

   765 in

   766   OuterSyntax.command "foobar" "proving a proposition" kind prove_prop

   766   OuterSyntax.command "foobar" "proving a proposition" kind prove_prop

   767 end *}

   767 end *}

   768 

   768 

   769 text {*

   769 text {*

   771   proved) and a context.  The context is necessary in order to be able to use

   771   proved) and a context.  The context is necessary in order to be able to use

   772   @{ML Syntax.read_prop}, which converts a string into a proper proposition.

   772   @{ML Syntax.read_prop}, which converts a string into a proper proposition.

   773   In Line 6 the function @{ML Proof.theorem_i} starts the proof for the

   773   In Line 6 the function @{ML Proof.theorem_i} starts the proof for the

   774   proposition. Its argument @{ML NONE} stands for a locale (which we chose to

   774   proposition. Its argument @{ML NONE} stands for a locale (which we chose to

   775   omit); the argument @{ML "(K I)"} stands for a function that determines what

   775   omit); the argument @{ML "(K I)"} stands for a function that determines what

   791   \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\

   791   \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\

   792   \isacommand{apply}@{text "(rule conjI)"}\\

   792   \isacommand{apply}@{text "(rule conjI)"}\\

   793   \isacommand{apply}@{text "(rule TrueI)+"}\\

   793   \isacommand{apply}@{text "(rule TrueI)+"}\\

   794   \isacommand{done}

   794   \isacommand{done}

   795   \end{isabelle}

   795   \end{isabelle}

   796 

   798 

   797   

   799   

   798   (FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?)

   800   (FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?)

   799 

   801 

   800   (FIXME read a name and show how to store theorems)

   802   (FIXME read a name and show how to store theorems)