src/Tools/jEdit/src/jedit_lib.scala
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) }