src/Tools/jEdit/src/jedit_lib.scala

--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 07 16:37:57 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 07 21:23:02 2014 +0200
@@ -120,6 +120,9 @@
   def jedit_buffer(name: String): Option[Buffer] =
     jedit_buffers().find(buffer => buffer_name(buffer) == name)
 
+  def jedit_buffer(name: Document.Node.Name): Option[Buffer] =
+    jedit_buffer(name.node)
+
   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
 
   def jedit_text_areas(view: View): Iterator[JEditTextArea] =