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-ste...@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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
