--- a/src/Tools/jEdit/src/jedit_lib.scala Mon Dec 01 17:51:07 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Mon Dec 01 19:25:20 2014 +0100
@@ -20,6 +20,7 @@
import org.gjt.sp.jedit.gui.KeyEventWorkaround
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
+import org.gjt.sp.jedit.syntax.TokenMarker
object JEdit_Lib
@@ -113,6 +114,12 @@
def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
+ def update_token_marker(buffer: JEditBuffer, marker: TokenMarker)
+ {
+ buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
+ buffer.setTokenMarker(marker)
+ }
+
/* main jEdit components */