--- 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