[isabelle-dev] print modes

[Christian Sternagel]

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