Email Gateway (Oct 12 2021 at 13:05): Email Gateway (Oct 12 2021 at 13:05):From: Daniel Kirchner <daniel@ekpyron.org>
Hi,
Sorry, if this has come up before, but I'm wondering about the
following:
consts test :: ‹'a ⇒ 'b ⇒ 'c›
notation test (infixl ‹→› 8)
syntax test :: ‹any ⇒ any ⇒ any› (infixl ‹↦› 8)
term ‹x → y›
term ‹x ↦ y›
Apparently the arrow in the first term that was introduced using
"notation", PIDE markup is generated associating the arrow with the
constant declaration of "test", i.e. the arrow is clickable in
Isabelle/jedit and links to the declaration of the constant "test".
However, the arrow in the second term, introduced by "syntax" does not
seem to produce similar markup information, e.g. it is not clickable in
Isabelle/jedit.
Looking at the PIDE markup information itself, I see both arrows
marked as "delimiter", but indeed only the former additionally getting an
entity reference to the constant definition.
I understand that "notation" and "syntax" work quite differently (and
"syntax" does not even necessarily refer to anything with a specific
declaration position), but I'm still wondering:
Is there currently any way to associate "syntax" with position markup
similarly to what "notation" does that I'm missing, possibly involving
Isabelle/ML?
If not, are there any plans for making this possible at least
"manually" or even for automatically generating such markup, where
applicable? Automatically might be tricky, e.g. I'd want to specify
that a purely syntactic constant "_test" refers to some specific
declaration as well, etc. - but "manually" even using ML would also
help. And even only referring to the position of the "syntax" command
itself might be better than having no associated position at all.
If not, I'd be eager to understand the issues involved and why this is
inherently more difficult for "syntax".
Best wishes,
Daniel Kirchner
Last updated: Jan 04 2025 at 20:18 UTC