[isabelle-dev] Deprecating legacy ASCII symbols?

[Jasmin Blanchette]

Makarius wrote:

>  * Convenience: users somethings find it too combersome to type proper
>    Isabelle symbols.
> 
>    I never do that myself, but take the time to type things nicely.  It
>    is actually not much time for me, since I implemented the input
>    methods myself and know how they work.

Today we have at least three concepts:

    ASCII symbols—e.g., <->
    xsymbols—e.g., \<longleftrightarrow>
    typing shortcuts (or whatever they are called)—e.g., <-> or <-->

To be complete, I should mention that xsymbols appear in two variants: the backslash-less-than-greater-than variant, the Unicode-like symbol one gets in jEdit. There used to be a third, wrong variant, at least in Proof General: the actual Unicode symbol, which paradoxically didn’t work when copy-pasted back from e.g. an email. (This is no longer an issue?)

This apparatus is rather heavy on beginners, and even experts will sometimes pause for a second to wonder whether they want to type :: or \<Colon> or whatever. I suspect one reason why John Harrison is so fast is that in HOL Light you don’t have to make such trivial decisions all the time.

Hence, I would be in favor of any process towards simplifying the situation. In particular, phasing out ASCII symbols gradually (and is as much this is possible w.r.t. compatibility) would make a lot of sense to me, as long as the corresponding typing shortcuts stay (and are documented).

Jasmin