[isabelle-dev] Deprecating legacy ASCII symbols?
nipkow at in.tum.de
Tue Jun 30 16:26:24 CEST 2015
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.
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5112 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev