Re: [isabelle] New commands in Isabelle2012



Dear all,

when following section 5.8 of the Progtutorial in jEdit, I noticed that a string that was declared as keyword in the keywords-section of the header is still highlighted as such after removing it from the keywords-section.

To reproduce start with:
--------------------------------
theory Foo imports Main begin
foobar
end
--------------------------------
where "foobar" is not highlighted as keyword. Now add
--------------------------------
keywords "foobar" :: thy_decl
--------------------------------
to the header. At this point "foobar" is highlighted as keyword (and something seems to happen at foobar, since the background is highlighted from there until the end of the file, but there is no output, which is also strange).

Now delete "foobar" from the content and remove the keywords-section again. When typing "foobar" again, it is still highlighted as keyword (and the usual "Outer syntax error: command expected, but identifier foobar was found" is missing).

cheers

chris

On 06/18/2012 11:06 PM, Christian Urban wrote:

Hi Dmitriy,

Thanks a lot! I updated the section accordingly
and also my own code in Nominal.

Thanks again,
Christian


On Sunday, June 17, 2012 at 08:03:49 (+0100), Dmitriy Traytel wrote:
  > Hi Christian,
  >
  > one could also mention the @{command_spec foobar} antiquotation which
  > allows you to avoid the duplication of the kind declaration in the code.
  >
  > Best wishes,
  > Dmitriy
  >
  > Am 17.06.2012 00:16, schrieb Christian Urban:
  > > On Saturday, June 16, 2012 at 16:46:04 (+0100), Omar Montaño Rivas wrote:
  > >   >  >
  > >   >  >  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.
  > >
  > > I took the opportunity to update this section.
  > > If you happen to have any feedback, I am grateful
  > > to receive it.
  > >
  > > Best wishes,
  > > Christian
  >








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