diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-19 09:12:12 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-19 09:12:12 +0000 |
| commit | 133453ff0339ea7fe3007022ba4a0a5259e339ca (patch) | |
| tree | fc9dc9ad54915c1a142c21b8e283ceeb9ce1eb7e /etc/isar | |
| parent | 98dc7edd17b2f2e638bf30b6d6d4faa1123609db (diff) | |
Clarify behaviour of copy-paste for token variants: it works fine in PG
Diffstat (limited to 'etc/isar')
| -rw-r--r-- | etc/isar/TokensAcid.thy | 12 |
1 files 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 "\<And1> {True, False}" term "\<And2> {\<lambda> x. True, \<lambda> y. False}" -(* Note: of course, copy and paste will produce wrong result - for above: default token <And> without variant is produced! *) - +(* Note: of course, copy and paste using Unicode to another + application (Tokens \<rightarrow> 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 |