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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
