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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
