paranoia null check -- prevent spurious crash of jedit token markup;
authorwenzelm
Sat, 14 Jan 2012 15:44:44 +0100
changeset 46210 553ec602d337
parent 46209 aad604f74be0
child 46211 2616e68877c9
paranoia null check -- prevent spurious crash of jedit token markup;
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) =