src/Tools/jEdit/src/token_markup.scala
changeset 53274 1760c01f1c78
parent 53249 c95e9aee959c
child 53277 6aa348237973
--- a/src/Tools/jEdit/src/token_markup.scala	Thu Aug 29 10:24:43 2013 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Thu Aug 29 12:38:33 2013 +0200
@@ -285,10 +285,7 @@
   def refresh_buffer(buffer: JEditBuffer)
   {
     buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
-    // FIXME potential NPE ahead!?!
-    val mode = buffer.getMode
-    val name = mode.getName
-    val marker = markers.get(name)
+    val marker = markers.get(JEdit_Lib.buffer_mode(buffer))
     marker.map(buffer.setTokenMarker(_))
   }
 }