[isabelle-dev] Deprecating legacy ASCII symbols?
makarius at sketis.net
Tue Jun 30 14:13:02 CEST 2015
On Tue, 30 Jun 2015, C. Diekmann wrote:
> In HOL.thy, the conjunction (conj) is first introduced with the "&"
> symbol. Later, the notation "∧" is introduced. In order to clean up
> this difficult-to-understand theory, would it be possible to directly
> introduce conjunction with the "∧" symbol? I see three advantages:
> 1) It simplifies the axiomatizations (a very critical part).
> 2) It may help in getting started with Isabelle since no confusing "&"
> symbol would appear anywhere. Currently, if a ctrl-click on a lemma
> sends me to HOL.thy, things look pretty scary.
> 3) It would free up the symbol "&" for custom theories.
> This could also be done for %, -->, ==, ~, and many more.
Interesting that you call this "legacy ASCII" syntax. In the manner it is
done until today, the ASCII syntax is still the official syntax and the
"xsymbols" variant some add-on. Only recently, the system default has
changed to have "xsymbols" always enabled by default.
Historically, there were good reasons of having the system act in plain
ASCII by default, due to a general lack of reliability in rendering
Isabelle symbols on various operating systems, terminal emulators, and
versions of Emacs.
Now that the TTY loop and Proof General are removed, there is nothing to
prevent a fresh look at the situation. Here are just the canonical
questions (which are never meant rhetoric):
(1) Are there remaining uses of plain ASCII syntax in Isabelle output?
(2) Are there remaining uses of plain ASCII syntax in Isabelle input?
As a start to the collection of material some possible points:
* Seemingly modern web frameworks might lack Unicode rendering quality
to work with Isabelle symbols relibly. 1-2 years ago there were still
problems on Stackoverflow. Do they still exist?
In contrast, plain HTML pages should be able to provide the
IsabelleText font from the server side. There is no need for the old
"HTML" print mode.
* Compatibility: huge amounts of existing sources still use ASCII input.
There are chances to make a systematic upgrade for formally checked
text, but not for unchecked comments.
* Convenience: users somethings find it too combersome to type proper
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.
Anything further points?
Once the collection of observation is complete, we can come up with
further migration plans to improve on the historical situation.
More information about the isabelle-dev