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

[Tobias Nipkow]

Am 17/04/2012 16:13, schrieb Makarius:
> On Tue, 17 Apr 2012, Tobias Nipkow wrote:
>> 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.

Calling "--" as opposed to "-" unwieldy is a bit of a joke. And provided the
editor supports the conversion to proper symbols nicely, it is merely a question
of typing, not reading.

> 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.

I have not experienced those difficulties.

> 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.

Not in ProofGeneral. I type -->  and it becomes \<longrightarrow>.

> 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.

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.

> I have seen pretty good mathematical input methods somewhere before, maybe in
> TeXmacs, maybe in some computer-algebra system.

I checked out TeXmacs and, surprise, surprise, when you type <-> it is converted
into \leftrightarrow, and when you type <--> it becomes \longleftrightarrow.

Tobias

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