# HG changeset patch
# User wenzelm
# Date 1377709691 -7200
# Node ID c95e9aee959ce93c6df3a7e922475cacb046361c
# Parent  7a4b4b3b9ecdb7aaf9ebf40204d1674dd4b1ed9f
tuned -- help finding rare NPE on cold start;

diff -r 7a4b4b3b9ecd -r c95e9aee959c src/Tools/jEdit/src/token_markup.scala
--- 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(_))
   }
 }