[isabelle] Declaration position markup with "notation", but not with "syntax"



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

Attachment: pgpHsBPP2JzEZ.pgp
Description: Digitale Signatur von OpenPGP



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