From 133453ff0339ea7fe3007022ba4a0a5259e339ca Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 19 Aug 2010 09:12:12 +0000 Subject: Clarify behaviour of copy-paste for token variants: it works fine in PG --- etc/isar/TokensAcid.thy | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/etc/isar/TokensAcid.thy b/etc/isar/TokensAcid.thy index 30807b89..c7129c0c 100644 --- a/etc/isar/TokensAcid.thy +++ b/etc/isar/TokensAcid.thy @@ -160,9 +160,15 @@ notation (xsymbols) term "\ {True, False}" term "\ {\ x. True, \ y. False}" -(* Note: of course, copy and paste will produce wrong result - for above: default token without variant is produced! *) - +(* Note: of course, copy and paste using Unicode to another + application (Tokens \ Copy As Unicode) and then re-reading in + Isabelle using another interface will probably produce wrong + result. But copy-pasting within Proof General Emacs is fine since + the underlying token text is copied, not the presentation. + What happens is that the text properties are "sticky" and + copied as well, so you see them even in non-Unicode Tokens buffers. + But if you save and revisit, you'll see the real text. +*) (* NB: below here cannot be processed: just in terms to check with -- cgit v1.2.3