Email Gateway (Aug 22 2022 at 19:28): Email Gateway (Aug 22 2022 at 19:28):From: Dominique Unruh <unruh@ut.ee>
Hi,
in jEdit, one can type, e.g., \typ to autocomplete to \<^typ><...>. But
\const does not work for getting \<^const>. (Note: the \<^const>
antiquotation accepts cartouches, but only when the constant is not
polymorphic. E.g., \<^const><bla> works, \<^const><blu(int)> does not,
@{const bla} and @{const blu(int)} both work.)
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 19:29):From: Makarius <makarius@sketis.net>
Thanks for pointing this out, I will polish this detail further.
Note that we are presently in a transition of antiquotation notation:
many applications already work more smoothly in the new (short) form
\<^name>CARTOUCHE, but some still do require the old one, because there
is more than one cartouche argument. Right now that duality of syntax is
still considered normal, but I find it myself more and more awkward to
work with the old @{name ARGS ...} form (e.g. for @{thm}, @{lemma},
@{cite}). In principle that could be eliminated by internalizing the
former syntax into a single cartouche argument, while keeping the old
syntax inside -- it is probably better to make slight reforms on syntax
at the same time.
Specifically for @{const name(type)} I would say we need proper inner
syntax for such type application to polymorphic constants. This would
help many applications within the regular term language. It is merely a
matter to find funny parentheses that can be rendered in LaTeX and some
free TrueType font: we can then add that to our infinite store of
Isabelle symbols and provide glyphs in the Isabelle fonts. (That is
definitely for a release after Isabelle2019.)
Makarius
Last updated: Nov 21 2024 at 12:39 UTC