[isabelle-dev] Deprecating legacy ASCII symbols?

[Tobias Nipkow]

I have no objection to phasing out some of the ASCII symbols. For me the main 
advantage is that they provide a graphic image that one can quickly recall as an 
input shortcut: ==> comes to mind more quickly than some alphabetic name and I 
would not want to lose that. But freeing them up in the input syntax (as opposed 
to the shortcuts) is not much of a gain because one cannot reasonably reuse 
them. But there is indeed quite a bit of duplication, eg & and /\, | and \/.

Some symbols like ! and ? are quick to type but I wouldn't call them "graphical" 
and am not particularly attached to them. In fact, one could then give factorial 
its standard syntax.

Tobias

On 30/06/2015 14:13, Makarius wrote:
> 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
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5112 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150630/d247a110/attachment.bin>