[isabelle-dev] print modes

[Makarius]

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