src/Tools/jEdit/src/pretty_text_area.scala

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 24 18:34:47 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 24 19:01:08 2012 +0100
@@ -92,17 +92,12 @@
 
           Swing_Thread.later {
             current_rendering = rendering
-
-            try {
-              getBuffer.beginCompoundEdit
+            JEdit_Lib.buffer_edit(getBuffer) {
               getBuffer.setReadOnly(false)
               setText(text)
               setCaretPosition(0)
               getBuffer.setReadOnly(true)
             }
-            finally {
-              getBuffer.endCompoundEdit
-            }
           }
         }))
     }