From 9204dbdd2d3d4b6c6aa7c2a3bb0fdd819c558c2a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 1 Oct 1999 10:10:04 +0000 Subject: Bug about cut-and-paste from highlighted Isabelle goals. --- BUGS | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'BUGS') diff --git a/BUGS b/BUGS index b821485f..33fef98e 100644 --- a/BUGS +++ b/BUGS @@ -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. + -- cgit v1.2.3