src/Tools/jEdit/src/jedit_lib.scala
changeset 50195 863b1dfc396c
parent 50186 f83cab68c788
child 50215 97959912840a
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 24 18:34:47 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 24 19:01:08 2012 +0100
     1.3 @@ -98,6 +98,12 @@
     1.4      finally { buffer.readUnlock() }
     1.5    }
     1.6  
     1.7 +  def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
     1.8 +  {
     1.9 +    try { buffer.beginCompoundEdit(); body }
    1.10 +    finally { buffer.endCompoundEdit() }
    1.11 +  }
    1.12 +
    1.13  
    1.14    /* point range */
    1.15