src/Tools/jEdit/src/jedit_lib.scala
changeset 53274 1760c01f1c78
parent 53247 bd595338ca18
child 53712 ea51046be71b
equal deleted inserted replaced
53273:473ea1ed7503 53274:1760c01f1c78
   128   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
   128   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
   129     Swing_Thread.now { buffer_lock(buffer) { body } }
   129     Swing_Thread.now { buffer_lock(buffer) { body } }
   130 
   130 
   131   def buffer_text(buffer: JEditBuffer): String =
   131   def buffer_text(buffer: JEditBuffer): String =
   132     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
   132     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
       
   133 
       
   134   def buffer_mode(buffer: JEditBuffer): String =
       
   135   {
       
   136     val mode = buffer.getMode
       
   137     if (mode == null) ""
       
   138     else {
       
   139       val name = mode.getName
       
   140       if (name == null) "" else name
       
   141     }
       
   142   }
   133 
   143 
   134   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
   144   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
   135 
   145 
   136 
   146 
   137   /* main jEdit components */
   147   /* main jEdit components */