src/Tools/jEdit/src/jedit_lib.scala
changeset 53274 1760c01f1c78
parent 53247 bd595338ca18
child 53712 ea51046be71b
--- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 29 10:24:43 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 29 12:38:33 2013 +0200
@@ -131,6 +131,16 @@
   def buffer_text(buffer: JEditBuffer): String =
     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
 
+  def buffer_mode(buffer: JEditBuffer): String =
+  {
+    val mode = buffer.getMode
+    if (mode == null) ""
+    else {
+      val name = mode.getName
+      if (name == null) "" else name
+    }
+  }
+
   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath