[isabelle-dev] print modes

[Makarius]

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.

Anyway, what are your remaining applications for ASCII notation?


> 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