Re: [isabelle] New commands in Isabelle2012



Hi Omar,

That is a part that has recently changed (like 2 - 3 months
ago) and I just did not have time to update the text. Though
the sources of the cookbook are updated.

If you use jEdit then the proof-script below will work. The 
difference is that the theory header now needs a declaration 
like

  keywords "foobar" :: thy_decl 

depending what kind of command you are defining.

If you use Emacs and Proof-General, you also have to now give
this declaration and in addition have to jump through the
hops of generating keyword files (as explained in the text).

Hope this helps,
Christian 





On Friday, June 15, 2012 at 23:17:15 (+0100), Omar Montaño Rivas wrote:
 > Hi all,
 > 
 > I am trying to define a custom Isar command in Isabelle 2012. I am
 > using the following example from Christian Urban's cookbook:
 > 
 > ML {*
 >       let
 >         val do_nothing = Scan.succeed (Local_Theory.background_theory I)
 >         val kind = Keyword.thy_decl
 >       in
 >         Outer_Syntax.local_theory ("foobar", kind) "description of foobar"
 >                                   do_nothing
 >       end
 > *}
 > 
 > However, I always get the error message:
 > 
 >  *** Undeclared outer syntax command "foobar"
 >  ***
 > 
 > Anybody know what I am doing wrong?
 > 
 > Thanks,
 > 
 > Omar.
 > 

-- 
theory Scratch
imports Main
keywords "foobar" :: thy_decl 
   
begin

ML {*
let
   val do_nothing = Scan.succeed (Local_Theory.background_theory I)
   val kind = Keyword.thy_decl
in
   Outer_Syntax.local_theory ("foobar", kind) "description of foobar" do_nothing
end
*}

foobar





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.