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