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

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

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

   945   by Proof-General. This results in some subtle configuration issues, which we will 

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

   949   Let us start with a ``silly'' command that does nothing at all. We

   949   at all. We shall name this command \isacommand{foobar}. On the ML-level it can be 

   950   shall name this command \isacommand{foobar}.  Before you can

   950   defined as:

   951   implement any new command, you have to ``announce'' it in the

   951 *}

   952   \isacommand{keyword}-section of theory header. For \isacommand{foobar}

   952 

   953   we need to write something like

   953 ML %grayML{*let

   954   val do_nothing = Scan.succeed (Local_Theory.background_theory I)

   955   val kind = Keyword.thy_decl

   956 in

   957   Outer_Syntax.local_theory ("foobar", kind) 

   958     "description of foobar" 

   959       do_nothing

   960 end *}

   961 

   962 text {*

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

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

   965   short description and a

   966   parser producing a local theory transition (its purpose will also explained

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

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

   969   to write

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

   962   whereby @{ML_ind "thy_decl" in Keyword} indicates the kind of the

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

   963   command.  Another possible kind is @{text "thy_goal"}, or you can

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

   964   also to omit the kind entirely, in which case you declare a keyword

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

   965   (something that is part of a command).

   982   you can type in your theory

   966 

   983 *}

   967   Now you can implement \isacommand{foobar} as:

   968 *}

   969 

   970 ML %grayML{*let

   971   val do_nothing = Scan.succeed (Local_Theory.background_theory I)

   972 in

   973   Outer_Syntax.local_theory @{command_spec "foobar"} 

   974     "description of foobar" 

   975       do_nothing

   976 end *}

   977 

   978 text {*

   979   The crucial function @{ML_ind local_theory in Outer_Syntax} expects

   980   the name for the command, a kind indicator, a short description and 

   981   a parser producing a local theory transition (explained later). For the

   982   name and the kind, you can use the ML-antiquotation @{text "@{command_spec ...}"}.

   983   After this, you can write in your theory 

   984 *}

   985 

   987 text {* 

   989 

   990 text {*

   991   Remember that this only works in jEdit. In order to let Proof-General 

   992   recognise this command, a keyword file needs to be generated (see next

   993   section).

   994 

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

   997   printing this proposition inside the tracing buffer. We announce the

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

   998   command as

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

   999 

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

  1000   \begin{graybox}

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

  1001   \isacommand{keywords} @{text [quotes] "foobar_trace"} @{text "::"} @{text "thy_decl"}

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

  1002   \end{graybox}

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

  1003 

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

  1004   The crucial part of a command is the function that determines the

   998   finally does nothing. For this you can write:

  1005   behaviour of the command. In the code above we used a

  1006   ``do-nothing''-function, which because of the parser @{ML_ind succeed in Scan}

  1007   does not parse any argument, but immediately returns the simple

  1008   function @{ML "Local_Theory.background_theory I"}. We can replace

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

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

  1011   (using the function @{text trace_prop}) and finally does

  1012   nothing. For this you can write:

  1004 

  1018 in

  1005   val kind = Keyword.thy_decl

  1019   Outer_Syntax.local_theory @{command_spec "foobar_trace"} 

  1006 in

  1007   Outer_Syntax.local_theory ("foobar_trace", kind) 

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

  1026   see the proposition in the tracing buffer.

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

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

  1044   it. Therefore, we need to announce this command in the header 

  1034   Keyword}.

  1045   as @{text "thy_goal"}

  1046 

  1047   \begin{graybox}

  1048   \isacommand{keywords} @{text [quotes] "foobar_goal"} @{text "::"} @{text "thy_goal"}

  1049   \end{graybox}

  1050 

  1051   Then we can write:

  1044   

  1061 in

  1045   val kind = Keyword.thy_goal

  1062   Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"}

  1046 in

  1047   Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) 

  1116   val kind = Keyword.thy_decl

  1207 in

  1117 in

  1208   Outer_Syntax.local_theory @{command_spec \"foobar\"}

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

  1234 ML {*

  1324 

  1235 structure Result = Proof_Data (

  1325 

  1236   type T = unit -> term

  1326 

  1237   fun init thy () = error "Result")

  1238 

  1239 val result_cookie = (Result.get, Result.put, "Result.put")

  1240 *}

  1241 

  1242 ML %grayML{*let

  1243    fun after_qed thm_name thms lthy =

  1244         Local_Theory.note (thm_name, (flat thms)) lthy |> snd

  1245 

  1246    fun setup_proof (thm_name, (txt, pos)) lthy =

  1247    let

  1248      val trm = Code_Runtime.value lthy result_cookie ("", txt)

  1249    in

  1250      Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy

  1251    end

  1252 

  1253    val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source

  1254  

  1255 in

  1256    Outer_Syntax.local_theory_to_proof ("foobar_prove", Keyword.thy_goal) 

  1257      "proving a proposition" 

  1258        (parser >> setup_proof)

  1259 end*}

  1260 

  1261 (*

  1262 foobar_prove test: {* @{prop "True"} *}

  1263 apply(rule TrueI)

  1264 done

  1265 *)