[isabelle-dev] Deprecating legacy ASCII symbols?
jasmin.blanchette at inria.fr
Tue Jun 30 16:07:11 CEST 2015
> * 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., <->
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).
More information about the isabelle-dev