src/Tools/jEdit/src/token_markup.scala
changeset 53274 1760c01f1c78
parent 53249 c95e9aee959c
child 53277 6aa348237973
equal deleted inserted replaced
53273:473ea1ed7503 53274:1760c01f1c78
   283   }
   283   }
   284 
   284 
   285   def refresh_buffer(buffer: JEditBuffer)
   285   def refresh_buffer(buffer: JEditBuffer)
   286   {
   286   {
   287     buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
   287     buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
   288     // FIXME potential NPE ahead!?!
   288     val marker = markers.get(JEdit_Lib.buffer_mode(buffer))
   289     val mode = buffer.getMode
       
   290     val name = mode.getName
       
   291     val marker = markers.get(name)
       
   292     marker.map(buffer.setTokenMarker(_))
   289     marker.map(buffer.setTokenMarker(_))
   293   }
   290   }
   294 }
   291 }
   295 
   292