578 While this is everything we have to do on the ML-level, we need a keyword |
578 While this is everything we have to do on the ML-level, we need a keyword |
579 file that can be loaded by ProofGeneral. This is to enable ProofGeneral to |
579 file that can be loaded by ProofGeneral. This is to enable ProofGeneral to |
580 recognise \isacommand{foobar} as a command. Such a keyword file can be |
580 recognise \isacommand{foobar} as a command. Such a keyword file can be |
581 generated with the command-line: |
581 generated with the command-line: |
582 |
582 |
583 |
|
584 @{text [display] "$ isabelle keywords -k foobar some_log_files"} |
583 @{text [display] "$ isabelle keywords -k foobar some_log_files"} |
585 |
584 |
586 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 |
587 will be assigned. In the case above the generated file will be named @{text |
586 will be assigned. In the case above the file will be named @{text |
588 "isar-keywords-foobar.el"}. As can be seen, this command requires log files to be |
587 "isar-keywords-foobar.el"}. As can be seen, this command requires log files to be |
589 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 |
590 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 |
591 @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the |
590 @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the |
592 complete code. |
591 complete code. |
606 in |
605 in |
607 OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing |
606 OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing |
608 end"}\\ |
607 end"}\\ |
609 \isa{\isacharverbatimclose}\\ |
608 \isa{\isacharverbatimclose}\\ |
610 \isacommand{end} |
609 \isacommand{end} |
611 \end{graybox}\\[-4mm] |
610 \end{graybox} |
612 \caption{\small The file @{text "Command.thy"} is necessary for generating a log |
611 \caption{\small The file @{text "Command.thy"} is necessary for generating a log |
613 file. This log file enables Isabelle to generate a keyword file containing |
612 file. This log file enables Isabelle to generate a keyword file containing |
614 the command \isacommand{foobar}.\label{fig:commandtheory}} |
613 the command \isacommand{foobar}.\label{fig:commandtheory}} |
615 \end{figure} |
614 \end{figure} |
616 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
615 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
679 of the directory is in @{text "$ISABELLE_LOGS"}, |
678 of the directory is in @{text "$ISABELLE_LOGS"}, |
680 then the Unix command for creating the keyword file is: |
679 then the Unix command for creating the keyword file is: |
681 |
680 |
682 @{text [display] |
681 @{text [display] |
683 "$ isabelle keywords -k foobar |
682 "$ isabelle keywords -k foobar |
684 $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}"} |
685 |
684 |
686 The result is the file @{text "isar-keywords-foobar.el"}. It should contain the |
685 The result is the file @{text "isar-keywords-foobar.el"}. It should contain |
687 string @{text "foobar"} twice (check for example that @{text "grep foobar |
686 the string @{text "foobar"} twice (to see whether things went wrong, check |
688 isar-keywords-foobar.el"} returns something non-empty). This keyword file |
687 that @{text "grep foobar"} on this file returns something |
689 needs to be copied into the directory @{text "~/.isabelle/etc"}. To make |
688 non-empty). This keyword file needs to |
690 Isabelle aware of this keyword file, we have to start Isabelle with the option @{text |
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 |
691 "-k foobar"}, i.e. |
691 "-k foobar"}, i.e. |
|
692 |
692 |
693 |
693 @{text [display] "$ isabelle -k foobar a_theory_file"} |
694 @{text [display] "$ isabelle -k foobar a_theory_file"} |
694 |
695 |
695 If we now build a theory on top of @{text "Command.thy"}, |
696 If we now build a theory on top of @{text "Command.thy"}, |
696 then we can make use of the command \isacommand{foobar}. |
697 then we can make use of the command \isacommand{foobar}. |
777 |
778 |
778 If we now type \isacommand{foobar}~@{text [quotes] "True \<and> True"}, we obtain the following |
779 If we now type \isacommand{foobar}~@{text [quotes] "True \<and> True"}, we obtain the following |
779 proof state: |
780 proof state: |
780 |
781 |
781 \begin{isabelle} |
782 \begin{isabelle} |
782 \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\ |
783 \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\ |
783 @{text "goal (1 subgoal)"}\\ |
784 @{text "goal (1 subgoal)"}\\ |
784 @{text "1. True \<and> True"} |
785 @{text "1. True \<and> True"} |
785 \end{isabelle} |
786 \end{isabelle} |
786 |
787 |
787 and we can build the proof |
788 and we can build the proof |
788 |
789 |
789 \begin{isabelle} |
790 \begin{isabelle} |
790 \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\ |
791 \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\ |
791 \isacommand{apply}@{text "(rule conjI)"}\\ |
792 \isacommand{apply}@{text "(rule conjI)"}\\ |
792 \isacommand{apply}@{text "(rule TrueI)+"}\\ |
793 \isacommand{apply}@{text "(rule TrueI)+"}\\ |
793 \isacommand{done} |
794 \isacommand{done} |
794 \end{isabelle} |
795 \end{isabelle} |
795 |
796 |
796 |
797 |
797 (FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?) |
798 (FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?) |
798 |
799 |
799 (FIXME Explain @{text "OuterKeyword.thy_decl"} and parser) |
|
800 |
|
801 (FIXME read a name and show how to store theorems) |
800 (FIXME read a name and show how to store theorems) |
802 |
801 |
803 (FIXME possibly also read a locale) |
802 (FIXME possibly also read a locale) |
804 *} |
803 *} |
805 |
804 |
806 (*<*) |
805 (*<*) |
|
806 |
807 chapter {* Parsing *} |
807 chapter {* Parsing *} |
808 |
808 |
809 text {* |
809 text {* |
810 |
810 |
811 Lots of Standard ML code is given in this document, for various reasons, |
811 Lots of Standard ML code is given in this document, for various reasons, |