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

[Makarius]

On Tue, 17 Apr 2012, Tobias Nipkow wrote:

> In HOL, the ASCII syntax for \<longleftrightarrow> is defined to be <-> 
> but visually <--> would be more appropriate, closer to -->

A brief look at the history and source archive shows that this ASCII art 
has already been there since Isabelle86. Larry might still remember his 
motivations in the depths of time.  I've always understood <-> as 
"visually appropriate" counterpart of --> in the sense of the physical 
length, despite the optical distortion since ASCII < > are not proper 
arrow heads.

Our default symbol mapping then associates long arrows of the same length 
accordingly, this time without optical distortions due to good quality 
IsabelleText or STIX fonts.


> and would also leave room for an ASCII syntax for \<leftrightarrow> 
> (namely <->).

Using <--> for <-> and making room for another <-> would also mean that 
the user has to type/read the longer unwieldy sequence by default.


Anyway, what is the role of the ASCII replacement syntax today?  We use it 
both for prover syntax and input methods of the editor, which I always 
find difficult to explain to new users.  In practice the alternative ASCII 
input is mainly passed to the prover because the editor completion 
mechanisms are still require an effort to change focus and press extra 
keys.

A really smooth input method in the editor could overcome the need for 
ASCII replacement syntax altogether.  Such input method could also admit 
multiple associations, e.g the user typing short <-> would get a selection 
of arrows to be inserted into the text.  (I used to have this in 
etc/symbols until some NICTA guys asked to make it unique again, to 
accomodate WWW_Find.)

I have seen pretty good mathematical input methods somewhere before, maybe 
in TeXmacs, maybe in some computer-algebra system.  This would mean a 
conceptual advance, not just a variation of old conventions.  I.e. we 
could overcome alternative syntax tables eventually.


 	Makarius