[isabelle-dev] Deprecating legacy ASCII symbols?

[Makarius]

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:

Concerning output:

   * 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.

Concerning input:

   * 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
     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.

Anything further points?

Once the collection of observation is complete, we can come up with 
further migration plans to improve on the historical situation.


 	Makarius