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

Makarius makarius at sketis.net
Tue Apr 17 19:51:26 CEST 2012

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 

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 

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


More information about the isabelle-dev mailing list