diff -r 5c7ade7a1e74 -r 2d39c313f39e src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Mon Apr 28 15:22:57 2014 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Mon Apr 28 15:29:09 2014 +0200 @@ -94,9 +94,6 @@ /* buffers */ - def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = - Swing_Thread.now { buffer_lock(buffer) { body } } - def buffer_text(buffer: JEditBuffer): String = buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }