[isabelle-dev] <-> and <-->
krauss at in.tum.de
Tue Apr 17 19:13:01 CEST 2012
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.
More information about the isabelle-dev