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 | |
parent | 8ca4face75e4a49bb7c41060130425bc13cfbc87 (diff) |
Bug about cut-and-paste from highlighted Isabelle goals.
-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. + |