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

[Makarius]

On Tue, 17 Apr 2012, Alexander Krauss wrote:

> 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 :-)

We all know these bad jokes of both Emacs and jEdit.  But the general 
problem of mathematical input has been studied by other people before -- I 
often see snippets of that at the CICM conference.  Even just for plain 
JVM-based IDE-style editing there are better solutions than the Sidekick 
popup that I am still using in Isabelle/jEdit (which was easy to set up in 
30min).

Anybody who feels like contributing constructively, should do a survey of 
the possibilities on the JVM platform and propose an suitable improvement 
of the Isabelle/jEdit completion mechanism.  Ideally with a little Scala 
implementation.


Concerning the situation in Isabelle/ProofGeneral right now: it is 
unmaintained so nothing can move there for this release.


 	Makarius