[isabelle-dev] <-> and <-->

[Alexander Krauss]

On 04/17/2012 05:41 PM, Tobias Nipkow wrote:
> This is what I would call unwieldy: instead of typing<-->  or<->  (and having
> them converted to the appropriate symbols) you always type<->, but then you
> have to select from a menue. I don't see the progress.

Could not agree more. These arrows are very common, and I want to be 
able to type them without menu interaction. The selection idea is the 
equivalent of "instead of having to use the shift key, you simply type 
the letter and then select from the menu whether you want the capital or 
the small letter".

Of course we should not forget that the eager replacement done by 
PG/Emacs is also problematic: try to type ~~/src and see how many 
keystrokes you need :-)

Maybe the "Isabelle Keyboard" from 2008 needs a revival in jEdit: It has 
an extra modifier key (a modded Windows key) which opens up a whole 
range of characters. But this is probably hard to do cross-platform.

Alex