[isabelle-dev] print modes
c-sterna at jaist.ac.jp
Fri May 11 11:33:24 CEST 2012
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.
More information about the isabelle-dev