src/Tools/jEdit/src/plugin.scala
changeset 44580 3bc9a215a56d
parent 44577 96b6388d06c4
child 44606 b625650aa2db
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 30 12:24:55 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 30 15:43:27 2011 +0200
     1.3 @@ -159,10 +159,27 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* buffers */
     1.8 +
     1.9 +  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    1.10 +    Swing_Thread.now { buffer_lock(buffer) { body } }
    1.11 +
    1.12 +  def buffer_text(buffer: JEditBuffer): String =
    1.13 +    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    1.14 +
    1.15 +  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    1.16 +
    1.17 +  def buffer_path(buffer: Buffer): (String, String) =
    1.18 +    (buffer.getDirectory, buffer_name(buffer))
    1.19 +
    1.20 +
    1.21    /* main jEdit components */
    1.22  
    1.23    def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
    1.24  
    1.25 +  def jedit_buffer(name: String): Option[Buffer] =
    1.26 +    jedit_buffers().find(buffer => buffer_name(buffer) == name)
    1.27 +
    1.28    def jedit_views(): Iterator[View] = jEdit.getViews().iterator
    1.29  
    1.30    def jedit_text_areas(view: View): Iterator[JEditTextArea] =
    1.31 @@ -180,17 +197,6 @@
    1.32      finally { buffer.readUnlock() }
    1.33    }
    1.34  
    1.35 -  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    1.36 -    Swing_Thread.now { buffer_lock(buffer) { body } }
    1.37 -
    1.38 -  def buffer_text(buffer: JEditBuffer): String =
    1.39 -    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    1.40 -
    1.41 -  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    1.42 -
    1.43 -  def buffer_path(buffer: Buffer): (String, String) =
    1.44 -    (buffer.getDirectory, buffer_name(buffer))
    1.45 -
    1.46  
    1.47    /* document model and view */
    1.48