src/Tools/jEdit/src/jedit_lib.scala
changeset 53274 1760c01f1c78
parent 53247 bd595338ca18
child 53712 ea51046be71b
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 29 10:24:43 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 29 12:38:33 2013 +0200
     1.3 @@ -131,6 +131,16 @@
     1.4    def buffer_text(buffer: JEditBuffer): String =
     1.5      buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
     1.6  
     1.7 +  def buffer_mode(buffer: JEditBuffer): String =
     1.8 +  {
     1.9 +    val mode = buffer.getMode
    1.10 +    if (mode == null) ""
    1.11 +    else {
    1.12 +      val name = mode.getName
    1.13 +      if (name == null) "" else name
    1.14 +    }
    1.15 +  }
    1.16 +
    1.17    def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    1.18  
    1.19