938 section {* New Commands and Keyword Files\label{sec:newcommand} *}

   938 section {* New Commands\label{sec:newcommand} *}

   942   need to be implemented. While this is not difficult on the ML-level,

   942   need to be implemented. While this is not difficult on the ML-level and

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

   943   jEdit, in order to be compatible, new commands need also to be recognised 

   944   ProofGeneral. This results in some subtle configuration issues, which we

   944   by ProofGeneral. This results in some subtle configuration issues, which we will 

   945   will explain in this section.

   945   explain in the next section. Here we just describe how to define new commands

   946 

   946   to work with jEdit.

   947   To keep things simple, let us start with a ``silly'' command that does nothing 

   947 

   948   Let us start with a ``silly'' command that does nothing 

   956   Outer_Syntax.local_theory ("foobar", kind) "description of foobar" do_nothing

   957   Outer_Syntax.local_theory ("foobar", kind) 

   958     "description of foobar" 

   959       do_nothing

   960   The crucial function @{ML_ind local_theory in Outer_Syntax} expects a name for the command, a

   963   The crucial function @{ML_ind local_theory in Outer_Syntax} expects a name for the command, 

   961   short description, a kind indicator (which we will explain later more thoroughly) and a

   964   a kind indicator (which we will explain later more thoroughly), a

   965   short description and a

   963   later). 

   967   later). Before you can use any new command, you have to ``announce'' it in the

   964 

   968   \isacommand{keyword}-section of theory header. In our running example we need

   965   While this is everything you have to do on the ML-level, you need a keyword

   969   to write

   966   file that can be loaded by ProofGeneral. This is to enable ProofGeneral to

   970 

   967   recognise \isacommand{foobar} as a command. Such a keyword file can be

   971   \begin{graybox}

   968   generated with the command-line:

   972   \isacommand{theory}~@{text Foo}\\

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

   974   \isacommand{keywords} @{text [quotes] "foobar"} @{text "::"} @{text "thy_decl"}\\

   975   ...

   976   \end{graybox}

   977 

   978   whereby you have to declare again that the new keyword is of the appropriate

   979   kind---for \isacommand{foobar} it is @{text "thy_decl"}. Another possible kind 

   980   is @{text "thy_goal"} and also to omit the kind entirely, in which case you declare a 

   981   keyword (something that is part of a command). After you announced the new command, 

   982   you can type in your theory

   983 *}

   984 

   985 foobar

   986 

   987 text {* 

   988   At the moment the command \isacommand{foobar} is not very useful. Let us

   989   refine it a bit next by letting it take a proposition as argument and

   990   printing this proposition inside the tracing buffer. For this the crucial 

   991   part of a command is the function that determines the behaviour

   992   of the command. In the code above we used a ``do-nothing''-function, which

   993   because of @{ML_ind succeed in Scan} does not parse any argument, but immediately

   994   returns the simple function @{ML "Local_Theory.background_theory I"}. We can

   995   replace this code by a function that first parses a proposition (using the

   996   parser @{ML Parse.prop}), then prints out some tracing

   997   information (using the function @{text trace_prop}) and 

   998   finally does nothing. For this you can write:

   999 *}

  1000 

  1001 ML %grayML{*let

  1002   fun trace_prop str = 

  1003     Local_Theory.background_theory (fn ctxt => (tracing str; ctxt))

  1004 

  1005   val kind = Keyword.thy_decl

  1006 in

  1007   Outer_Syntax.local_theory ("foobar_trace", kind) 

  1008     "traces a proposition" 

  1009       (Parse.prop >> trace_prop)

  1010 end *}

  1011 

  1012 text {*

  1013   The command is now \isacommand{foobar\_trace} and can be used to 

  1014   see the proposition in the tracing buffer (remember you need to announce

  1015   every new command in the header of the theory).  

  1016 *}

  1017 

  1018 foobar_trace "True \<and> False"

  1019 

  1020 text {*

  1021   Note that so far we used @{ML_ind thy_decl in Keyword} as the kind

  1022   indicator for the new command.  This means that the command finishes as soon as

  1023   the arguments are processed. Examples of this kind of commands are

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

  1025   are expected to parse some arguments, for example a proposition, and then

  1026   ``open up'' a proof in order to prove the proposition (for example

  1027   \isacommand{lemma}) or prove some other properties (for example

  1028   \isacommand{function}). To achieve this kind of behaviour, you have to use

  1029   the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML

  1030   "local_theory_to_proof" in Outer_Syntax} to set up the command. 

  1031   Below we show the command \isacommand{foobar\_goal} which takes a

  1032   proposition as argument and then starts a proof in order to prove

  1033   it. Therefore in Line 9, we set the kind indicator to @{ML thy_goal in

  1034   Keyword}.

  1035 *}

  1036 

  1037 ML%linenosgray{*let

  1038   fun goal_prop str ctxt =

  1039     let

  1040       val prop = Syntax.read_prop ctxt str

  1041     in

  1042       Proof.theorem NONE (K I) [[(prop, [])]] ctxt

  1043     end

  1044   

  1045   val kind = Keyword.thy_goal

  1046 in

  1047   Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) 

  1048     "proves a proposition" 

  1049       (Parse.prop >> goal_prop)

  1050 end *}

  1051 

  1052 text {*

  1053   The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be

  1054   proved) and a context as argument.  The context is necessary in order to be able to use

  1055   @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.

  1056   In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the

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

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

  1059   should be done with the theorem once it is proved (we chose to just forget

  1060   about it). 

  1061 

  1062   If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \<and> True"},

  1063   you obtain the following proof state:

  1064 *}

  1065 

  1066 foobar_goal "True \<and> True"

  1067 txt {*

  1068   \begin{minipage}{\textwidth}

  1069   @{subgoals [display]}

  1070   \end{minipage}\medskip

  1071 

  1072   and can prove the proposition as follows.

  1073 *}

  1074 apply(rule conjI)

  1075 apply(rule TrueI)+

  1076 done

  1077 

  1078 text {*

  1079   While this is everything you have to do for a new command when using jEdit, 

  1080   things are not as simple when using Emacs and ProofGeneral. We explain the details 

  1081   next.

  1082 *}

  1083 

  1084 

  1085 section {* Proof-General and Keyword Files *}

  1086 

  1087 text {*

  1088   In order to use a new command in Emacs and Proof-General, you need a keyword

  1089   file that can be loaded by ProofGeneral. To keep things simple we take as

  1090   running example the command \isacommand{foobar} from the previous section. 

  1091 

  1092   A keyword file can be generated with the command-line:

   993   Outer_Syntax.local_theory (\"foobar\", kind) \"description of foobar\" do_nothing

  1118   Outer_Syntax.local_theory (\"foobar\", kind) 

  1119     \"description of foobar\" 

  1120        do_nothing

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

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

  1084   then you can use the command \isacommand{foobar}. You can just write

  1211   then you can now use the command \isacommand{foobar}

  1085 *}

  1212   in Proof-General

  1086 

  1213 

  1087 foobar

  1214   A similar procedure has to be done with any 

  1088 

  1089 text {* 

  1090   but you will not see any action as we chose to implement this command to do

  1091   nothing. The point of this command is only to show the procedure of how

  1092   to interact with ProofGeneral. A similar procedure has to be done with any 

  1099 text {*

  1221 

  1100   At the moment the command \isacommand{foobar} is not very useful. Let us

  1222 text {*

  1101   refine it a bit next by letting it take a proposition as argument and

  1223   Also if the kind of a command changes, from @{text "thy_decl"} to 

  1102   printing this proposition inside the tracing buffer.

  1224   @{text "thy_goal"} say,  you need to recreate the keyword file.

  1103 

  1225 *}

  1104   The crucial part of a command is the function that determines the behaviour

  1105   of the command. In the code above we used a ``do-nothing''-function, which

  1106   because of @{ML_ind succeed in Scan} does not parse any argument, but immediately

  1107   returns the simple function @{ML "Local_Theory.background_theory I"}. We can

  1108   replace this code by a function that first parses a proposition (using the

  1109   parser @{ML Parse.prop}), then prints out the tracing

  1110   information (using a new function @{text trace_prop}) and 

  1111   finally does nothing. For this you can write:

  1112 *}

  1113 

  1114 ML %grayML{*let

  1115   fun trace_prop str = 

  1116      Local_Theory.background_theory (fn ctxt => (tracing str; ctxt))

  1117 

  1118   val kind = Keyword.thy_decl

  1119 in

  1120   Outer_Syntax.local_theory ("foobar_trace", kind) "traces a proposition" 

  1121     (Parse.prop >> trace_prop)

  1122 end *}

  1123 

  1124 text {*

  1125   The command is now \isacommand{foobar\_trace} and can be used to 

  1126   see the proposition in the tracing buffer.  

  1127 *}

  1128 

  1129 foobar_trace "True \<and> False"

  1130 

  1131 text {*

  1132   Note that so far we used @{ML_ind thy_decl in Keyword} as the kind

  1133   indicator for the command.  This means that the command finishes as soon as

  1134   the arguments are processed. Examples of this kind of commands are

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

  1136   are expected to parse some arguments, for example a proposition, and then

  1137   ``open up'' a proof in order to prove the proposition (for example

  1138   \isacommand{lemma}) or prove some other properties (for example

  1139   \isacommand{function}). To achieve this kind of behaviour, you have to use

  1140   the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML

  1141   "local_theory_to_proof" in Outer_Syntax} to set up the command.  Note,

  1142   however, once you change the ``kind'' of a command from @{ML thy_decl in

  1143   Keyword} to @{ML thy_goal in Keyword} then the keyword file needs

  1144   to be re-created!

  1145 

  1146   Below we show the command \isacommand{foobar\_goal} which takes a

  1147   proposition as argument and then starts a proof in order to prove

  1148   it. Therefore in Line 9, we set the kind indicator to @{ML thy_goal in

  1149   Keyword}.

  1150 *}

  1151 

  1152 ML%linenosgray{*let

  1153   fun goal_prop str lthy =

  1154     let

  1155       val prop = Syntax.read_prop lthy str

  1156     in

  1157       Proof.theorem NONE (K I) [[(prop, [])]] lthy

  1158     end

  1159   

  1160   val kind = Keyword.thy_goal

  1161 in

  1162   Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) "proves a proposition" 

  1163     (Parse.prop >> goal_prop)

  1164 end *}

  1165 

  1166 text {*

  1167   The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be

  1168   proved) and a context as argument.  The context is necessary in order to be able to use

  1169   @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.

  1170   In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the

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

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

  1173   should be done with the theorem once it is proved (we chose to just forget

  1174   about it). Line 9 contains the parser for the proposition.

  1175 

  1176   If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \<and> True"},

  1177   you obtain the following proof state

  1178 *}

  1179 

  1180 foobar_goal "True \<and> True"

  1181 txt {*

  1182   \begin{minipage}{\textwidth}

  1183   @{subgoals [display]}

  1184   \end{minipage}\medskip

  1185 

  1186   and can prove the proposition as follows.

  1187 *}

  1188 apply(rule conjI)

  1189 apply(rule TrueI)+

  1190 done

  1200 structure Result = Proof_Data(

  1235 structure Result = Proof_Data (

  1401 method_setup test = {* Scan.lift (Scan.succeed (K Method.succeed)) *} {* bla *}

  1436 method_setup test = {* 

  1437   Scan.lift (Scan.succeed (K Method.succeed)) *} {* bla *}

  1407 method_setup joker = {* Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *}

  1443 method_setup joker = {* 

  1444   Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *}