Re: [isabelle] New commands in Isabelle2012



Hi Christian,

On 16 June 2012 03:46, Christian Urban <christian.urban at kcl.ac.uk> wrote:
>
> 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

Yes, now it works in ProofGeneral. Thank you!

Omar.

>
> 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.