src/Tools/jEdit/src/jedit_lib.scala

--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 24 18:34:47 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 24 19:01:08 2012 +0100
@@ -98,6 +98,12 @@
     finally { buffer.readUnlock() }
   }
 
+  def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
+  {
+    try { buffer.beginCompoundEdit(); body }
+    finally { buffer.endCompoundEdit() }
+  }
+
 
   /* point range */