diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-10-01 10:10:04 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-10-01 10:10:04 +0000 |
| commit | 9204dbdd2d3d4b6c6aa7c2a3bb0fdd819c558c2a (patch) | |
| tree | ad3ccfcc00b9322df2b12ff63164beb33f43bffe /BUGS | |
| parent | 8ca4face75e4a49bb7c41060130425bc13cfbc87 (diff) | |
Bug about cut-and-paste from highlighted Isabelle goals.
Diffstat (limited to 'BUGS')
| -rw-r--r-- | BUGS | 7 |
1 files changed, 7 insertions, 0 deletions
@@ -165,3 +165,10 @@ Proof General will block the Emacs process when it is waiting for a theory file (and it's ancestors) to be read. To avoid this, assert the theory file rather than the ML file. +* Cut-and-paste from Isabelle output (e.g. goals buffer) is +problematic. You will find that this inserts otherwise-invisible +special characters into the script buffer, which are used to do the +highlighting. If you really need to do cut-and-paste, customize the +variable proof-shell-leave-annotations-in-output to nil. +Unfortunately this will turn off highlighting. + |