On Wed, 5 Mar 2014, Lars Noschinski wrote:
it would be nice if we could also get "<-" as abbreviation for
\<leftarrow> (and probably <-- for \<longleftarrow) by default.
\<leftarrow> is regularly used in Monad syntax and list comprehensions
and it would be nice to have the abbreviations matching the
rightarrow-variants.
I can't say on the spot how it would work out: the current scheme is the
result of intensive experimentation over some weeks last summer. This
needs to be repeated soon, when the semantic completion is fully
operational. Right now I am reworking again some details of that.
Did you try any of the catch-all abbreviations, like <. for left arrows,
or .> for right arrows, or <> for double arrows? These are very
ambiguous, but the persistent completion history will move your favourite
arrows to front, for quick access in the popup. Ambiguous completions are
never immediate, though.
It is also possible to add more abbreviations in
$ISABELLE_HOME_USER/etc/settings, although I consider that as something
for expert users only.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
