[isabelle-dev] Paste Deleted

Makarius makarius at sketis.net
Tue May 1 16:48:30 CEST 2018

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:

changeset:   68060:3931ed905e93
tag:         tip
user:        wenzelm
date:        Tue May 01 16:42:14 2018 +0200
files:       src/Tools/jEdit/src/jedit_lib.scala
avoid output showing up in kill ring (via TextArea.setText,
JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for
action "paste-deleted";

It uses an internal flag for the undo manager, so it might have
unexpected consequences. For now it looks fine, though.


More information about the isabelle-dev mailing list