[isabelle-dev] Abbreviation for \<leftarrow>

[Makarius]

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