Email Gateway (Aug 18 2022 at 12:59): Email Gateway (Aug 18 2022 at 12:59):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Dear Isabelle Users,
I have found that when including an ML file with:
"use blah.sml"
if I have an annotation like @{const_name "doesnt_exist"} in a
statement, then commenting it out doesn't stop the "unknown constant"
error when processing the ML file!
Is this behaviour intentional? Is there any way to actually comment out
a block of code AND its annotations?
Yours Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 12:59):From: Tobias Nipkow <nipkow@in.tum.de>
The reason is that antiquotations are processed separately. I'm not sure
if there is a better solution, but I always "disable" them individually
by removing the @ or putting a space after it. That does it. Not very
elegant.
Tobias
Rafal Kolanski schrieb:
Email Gateway (Aug 18 2022 at 13:04):From: Makarius <makarius@sketis.net>
On Thu, 12 Feb 2009, Rafal Kolanski wrote:
I have found that when including an ML file with:
"use blah.sml"
BTW, Isabelle/ML files should always be .ML -- not .sml
if I have an annotation like @{const_name "doesnt_exist"} in a statement,
then commenting it out doesn't stop the "unknown constant" error when
processing the ML file!Is this behaviour intentional? Is there any way to actually comment out a
block of code AND its annotations?
The behaviour is just a consequence of how ML antiquotations are done (not
"annotations"): as a preprecessing step before actual ML processing. In
particular, the antiquotation layer does not understand ML syntax, so
there is now chance to treat them differently inside ML comments.
At a later stage, antiquotations might be more tightly integrated with the
ML syntax. The motivation is more substantial though: allowing to write
ML patterns and expressions containing variables, e.g something like f
@{term "x + y"}
As a consequence of that future refinement, comments might be treated
differently as well.
Makarius
Last updated: May 03 2024 at 04:19 UTC