changeset 56774 | 2d39c313f39e |
parent 56699 | 60ad80f5cb62 |
child 56823 | 37be55461dbe |
--- 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) }