Re: [isabelle] unicode tokens in isabelle2011+pg4.0



On Wed, Feb 2, 2011 at 8:15 AM, Makarius <makarius at sketis.net> wrote:
> On Wed, 2 Feb 2011, Brian Huffman wrote:
>
>> On Tue, Feb 1, 2011 at 9:27 PM, Joachim Breitner
>> <mail at joachim-breitner.de> wrote:
>>>
>>> is there a reason why Isabelle would not accept ∀ synonymously to
>>> \<forall> in theory files? This would also be nice for all those
>>> unicode-loving folk who occasionally at .thy files directly (e.g. doing
>>> some mass-substitution with vim, or looking at diffs).
>>
>> You can certainly configure Isabelle to allow unicode as an alternative
>> input syntax. For example, you can define the following notation for the
>> forall-quantifier, where "∀" is a genuine unicode symbol instead of the
>> "\<forall>" markup:
>>
>> notation (input) All (binder "∀" 10)
>>
>> Now the genuine unicode forall symbol works as expected on input:
>>
>> term "∀x. P x"
>>
>> I suppose you could create a theory file that defines similar unicode
>> notation for all syntax defined in Isabelle/HOL. This might make a nice
>> addition to HOL/Library.
>
> This is a bad idea.  From what has been explained before, the Isabelle
> treatment of symbols vs. unicode handling assumes that this is not done. Big
> confusion is to be expected if this is violated.  (E.g. try to load such a
> file with Isabelle/jEdit and then save it again.)
>
> See also http://isabelle.in.tum.de/dist/Isabelle2011/doc/implementation.pdf
> section "1.2.1 Strings of Symbols" for some explanations and specifications
> around this important Isabelle concept.

In section 1.2.1 of the Implementation manual, it clearly states that
unicode codepoints like "∀" are treated distinctly from symbols like
"\<forall>". ProofGeneral 4.0 and 4.1 apparently respect this
distinction, while Isabelle/jEdit does not.

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.