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