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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
