On 04/04/18 14:33, Lawrence Paulson wrote:
> I sometimes like to use Edit > More Clipboard > Paste Deleted… to recover
> deleted material, but mostly it offers things like "proof (chain)
> picking this:…" that were automatically deleted from various panels. Do you
> think it would be difficult to change things so that Paste Deleted referred
> only to changes in the editor window?
[I am answering this on isabelle-dev, which is the canonical place to
discuss ongoing Isabelle development.]
See now the following change:
date: Tue May 01 16:42:14 2018 +0200
avoid output showing up in kill ring (via TextArea.setText,
JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for
It uses an internal flag for the undo manager, so it might have
unexpected consequences. For now it looks fine, though.
isabelle-dev mailing list