[isabelle-dev] <-> and <-->
nipkow at in.tum.de
Tue Apr 17 17:41:34 CEST 2012
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.
> This would mean a conceptual
> advance, not just a variation of old conventions. I.e. we could overcome
> alternative syntax tables eventually.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev