Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Declaration position markup with "notation", b...


view this post on Zulip 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:

Best wishes,
Daniel Kirchner


Last updated: Jul 15 2022 at 23:21 UTC