Re: [isabelle] [Isabelle 2019-RC0] jEdit support for \<^const>

On 22/04/2019 11:19, Dominique Unruh wrote:
> 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.)

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.)


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