# HG changeset patch
# User wenzelm
# Date 1525185734 -7200
# Node ID 3931ed905e932d387d20cef14c90df643f8eecca
# Parent  6f7829c14f5a41d49e850180c0b6467e179e7901
avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";

diff -r 6f7829c14f5a -r 3931ed905e93 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 30 22:13:21 2018 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue May 01 16:42:14 2018 +0200
@@ -129,6 +129,13 @@
 
   def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer))
 
+  def buffer_undo_in_progress[A](buffer: JEditBuffer, body: => A): A =
+  {
+    val undo_in_progress = buffer.isUndoInProgress
+    def set(b: Boolean) { Untyped.set[Boolean](buffer, "undoInProgress", b) }
+    try { set(true); body } finally { set(undo_in_progress) }
+  }
+
 
   /* main jEdit components */
 
diff -r 6f7829c14f5a -r 3931ed905e93 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Apr 30 22:13:21 2018 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue May 01 16:42:14 2018 +0200
@@ -144,7 +144,7 @@
             JEdit_Lib.buffer_edit(getBuffer) {
               rich_text_area.active_reset()
               getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
-              setText(text)
+              JEdit_Lib.buffer_undo_in_progress(getBuffer, setText(text))
               setCaretPosition(0)
             }
           }