[isabelle-dev] print modes

[Christian Sternagel]

On 05/08/2012 07:58 PM, Makarius wrote:
> On Wed, 2 May 2012, Brian Huffman wrote:
>
>> On Wed, May 2, 2012 at 6:55 AM, Christian Sternagel
>> <c-sterna at jaist.ac.jp> wrote:
>>> is it really the case that currently the only way to obtain ASCII output
>>> using print modes is by specifying the empty string, like
>>>
>>> thm ("") conjE
>>>
>>> or did I miss anything? Since this print mode is occasionally useful,
>>> I suggest to provide a named variant, like 'plain', 'ASCII', or
>>> whatever.
>
> The variety of print modes were introduced to overcome certain
> limitations of display capabilities. In a sense most of that is
> "legacy", but I've recently refurbished the description in the manual,
> see isar-ref section 7.1.3 in Isabelle2012-RC2. Mode "" is formally the
> default, the fall-back print mode.
I see.
>
> Anyway, what are your remaining applications for ASCII notation?
Currently only, copy-pasting examples from jedit into e-mails for the 
Isabelle mailing list ;). Not very convincing, is it?
>
>
>> I would actually go a bit further, and get rid of "xsymbol" as a
>> special syntax mode.
>>
>> It bothers me that if I want to define a constant with both ascii and
>> symbol notation, I have to use the ascii variant in the actual
>> definition, and then add the (far more commonly-used) symbol notation
>> later.
>>
>> definition foo :: "'a => 'a => bool" (infix "~~" 50) where ...
>> notation (xsymbol) foo (infix "\<approx>" 50)
>>
>> I would rather write:
>>
>> definition foo :: "'a => 'a => bool" (infix "\<approx>" 50) where ...
>> notation (ascii) foo (infix "~~" 50)
>
> In some sense "xsymbol" is merely a convention. Nothing stops you from
> inventing other print modes on the spot. Is is a matter of library
> organization how this is done in practice.
>
> Since plain symbol notation now works most of the time, both in the
> editor and in HTML, one could eventually move on to discontinue these
> special modes and use more symbols by default.
>
> Then there would be only one (symbol) notation for most things. For very
> basic things like !! ==> etc. this would require thoughts, though.
>
>
> Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev