src/Tools/jEdit/src/jedit_resources.scala
changeset 56457 eea4bbe15745
parent 56316 b1cf8ddc2e04
child 56460 af28fdd50690
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 07 16:37:57 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 07 21:23:02 2014 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4    override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
     1.5    {
     1.6      Swing_Thread.now {
     1.7 -      JEdit_Lib.jedit_buffer(name.node) match {
     1.8 +      JEdit_Lib.jedit_buffer(name) match {
     1.9          case Some(buffer) =>
    1.10            JEdit_Lib.buffer_lock(buffer) {
    1.11              Some(f(buffer.getSegment(0, buffer.getLength)))