[isabelle-dev] Paste Deleted

[Makarius]

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
src/Tools/jEdit/src/pretty_text_area.scala
description:
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.


	Makarius