On Wed, 2 May 2012, Brian Huffman wrote:
On Wed, May 2, 2012 at 6:55 AM, Christian Sternagel
<[email protected]> 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
