Re: [isabelle-dev] print modes
On Fri, 11 May 2012, Christian Sternagel wrote: You are right. However, if the "target" is a "newbie", it is often very important to have it _exactly_ as it has to be typed (which does not necessarily hold depending on syntax translations etc., even if the print mode is ""). We are back to the historic mix of several slightly different things: * prover input syntax * prover output syntax * physical rendering of the text encoding of the prover in the front-end * input methods to produce something that the prover will digest In Isabelle/jEdit (and the adjacent HTML output) things can be copy-pasted right now in most situations, even the sub-superscripts. I've spent quite some efforts on all this. If it does not work in Isabelle2012-RC, it is the proper time to point out the remaining problems now. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] print modes
On Fri, 11 May 2012, Lawrence Paulson wrote: I disagree. People frequently e-mail problems to one another. Of course, the ability to paste readable Unicode symbols would be even better, but that's surely too much to ask right now. Part of the hidden context of this thread is the front-end you are using. Some years ago, when the Proof General replacement project was started, Johannes Hölzl was one of the early students working on it. He asked about the main new features to be supported, and my spontaneous answer was: copy-and-paste. It is a long-standing running gag of Proof General / Emacs that it has its own peculiar ideas what copy-paste means. In Isabelle/jEdit it should work most of the time, and the cases where it does not are boundary situations, not the default as under the old regime. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] print modes
You are right. However, if the "target" is a "newbie", it is often very important to have it _exactly_ as it has to be typed (which does not necessarily hold depending on syntax translations etc., even if the print mode is ""). On 05/11/2012 06:21 PM, Makarius wrote: On Fri, 11 May 2012, Christian Sternagel wrote: 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 think most people now copy the Unicode from the physical rendering seen in the editor buffer or HTML view. This works most of the time. Formal text that is copy-pasted is approximative anyway, in the sense that it lacks the precise context. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] print modes
On Fri, 11 May 2012, Christian Sternagel wrote: 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 think most people now copy the Unicode from the physical rendering seen in the editor buffer or HTML view. This works most of the time. Formal text that is copy-pasted is approximative anyway, in the sense that it lacks the precise context. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] print modes
I disagree. People frequently e-mail problems to one another. Of course, the ability to paste readable Unicode symbols would be even better, but that's surely too much to ask right now. Larry On 11 May 2012, at 06:33, Christian Sternagel wrote: > Currently only, copy-pasting examples from jedit into e-mails for the > Isabelle mailing list ;). Not very convincing, is it? > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] print modes
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
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 "\" 50)
I would rather write:
definition foo :: "'a => 'a => bool" (infix "\" 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
Re: [isabelle-dev] print modes
On Wed, 2 May 2012, Brian Huffman wrote:
On Wed, May 2, 2012 at 6:55 AM, Christian Sternagel
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 "\" 50)
I would rather write:
definition foo :: "'a => 'a => bool" (infix "\" 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
Re: [isabelle-dev] print modes
On Wed, May 2, 2012 at 6:55 AM, Christian Sternagel
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.
+1
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 "\" 50)
I would rather write:
definition foo :: "'a => 'a => bool" (infix "\" 50) where ...
notation (ascii) foo (infix "~~" 50)
- Brian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] print modes
Dear all,
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.
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
