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)
             }
           }