[isabelle-dev] print modes
makarius at sketis.net
Tue May 8 12:58:15 CEST 2012
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
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
> 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.
More information about the isabelle-dev