Email Gateway (Aug 18 2022 at 20:19): Email Gateway (Aug 18 2022 at 20:19):From: Makarius <makarius@sketis.net>
On Tue, 19 Jun 2012, Christian Sternagel wrote:
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).
The command is declared as a keyword, but not defined yet, so some
undefined behaviour is to be expected. What happens here is that the
execution of that document version stops at the undefined command, since
the attempt to parse it semantically has failed.
I would say that is correct behaviour, although there could be more
ambitious error messages.
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).
I did not quite manage to reproduce that exactly. Nonetheless, some odd
effects are to be expected when declared command keywords are removed
later. This is because there are several slightly different ways to
manage commands at the same time: the old global table for the TTY loop
(and thus for Proof General) and a new value-oriented table within the
theory, moreover the the Prover IDE with its own syntax derived from the
keywords declarations in the theory headers without inspecting the
semantic content yet (intertwined with the editing process).
The whole affair is a bit like providing syntax highlighting for perl6,
and it works surprisingly well already. After a few more years, when the
TTY loop and PG are really obsolete, the old stateful way can disappear
altogether and become fully value-oriented without odd effects. But that
is not imminent. I have no reason to kill Proof General prematurely,
after so many years of tending it.
Makarius
Email Gateway (Aug 18 2022 at 20:25):From: Omar Montaño Rivas <omarmrivas@gmail.com>
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.
Email Gateway (Aug 18 2022 at 20:25):From: Christian Urban <christian.urban@kcl.ac.uk>
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
Email Gateway (Aug 18 2022 at 20:25):From: Omar Montaño Rivas <omarmrivas@gmail.com>
Hi Christian,
On 16 June 2012 03:46, Christian Urban <christian.urban@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
likekeywords "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,
ChristianOn 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_declbegin
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
Email Gateway (Aug 18 2022 at 20:26):From: Dmitriy Traytel <traytel@in.tum.de>
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
Email Gateway (Aug 18 2022 at 20:28):From: Christian Urban <christian.urban@kcl.ac.uk>
Hi Dmitriy,
Thanks a lot! I updated the section accordingly
and also my own code in Nominal.
Thanks again,
Christian
Email Gateway (Aug 18 2022 at 20:28):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Last updated: Apr 24 2024 at 16:18 UTC