diff -r 9f87eb298b75 -r 65babcd8b0e6 src/Tools/jEdit/src/jedit_lib.scala
--- 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 */