--- a/src/Tools/jEdit/src/token_markup.scala Wed Aug 28 17:20:16 2013 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Wed Aug 28 19:08:11 2013 +0200
@@ -285,7 +285,11 @@
def refresh_buffer(buffer: JEditBuffer)
{
buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
- markers.get(buffer.getMode.getName).map(buffer.setTokenMarker(_))
+ // FIXME potential NPE ahead!?!
+ val mode = buffer.getMode
+ val name = mode.getName
+ val marker = markers.get(name)
+ marker.map(buffer.setTokenMarker(_))
}
}