# HG changeset patch
# User wenzelm
# Date 1326552284 -3600
# Node ID 553ec602d337d4e8ed82965fd4d7c2f00c909eac
# Parent  aad604f74be0a74768757b3185613d17cf4d610a
paranoia null check -- prevent spurious crash of jedit token markup;

diff -r aad604f74be0 -r 553ec602d337 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sat Jan 14 15:30:54 2012 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Jan 14 15:44:44 2012 +0100
@@ -165,13 +165,15 @@
   class Marker extends TokenMarker
   {
     override def markTokens(context: TokenMarker.LineContext,
-        handler: TokenHandler, line: Segment): TokenMarker.LineContext =
+        handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
     {
       val line_ctxt =
         context match {
           case c: Line_Context => c.context
           case _ => Some(Scan.Finished)
         }
+      val line = if (raw_line == null) new Segment else raw_line
+
       val context1 =
       {
         val (styled_tokens, context1) =