# HG changeset patch
# User wenzelm
# Date 1246732137 -7200
# Node ID c620d8c7f6b35fcdf6be5cdabe638f8e70eeabdc
# Parent  051635fa7b7e0f178ca9119ac81ed35f46d1d86e
use symbolic NULL;

diff -r 051635fa7b7e -r c620d8c7f6b3 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sat Jul 04 17:50:48 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sat Jul 04 20:28:57 2009 +0200
@@ -60,7 +60,7 @@
       Markup.METHOD -> FUNCTION,
       // ML syntax
       Markup.ML_KEYWORD -> KEYWORD2,
-      Markup.ML_IDENT -> 0,
+      Markup.ML_IDENT -> NULL,
       Markup.ML_TVAR -> LITERAL3,
       Markup.ML_NUMERAL -> DIGIT,
       Markup.ML_CHAR -> LITERAL1,
@@ -74,7 +74,7 @@
       Markup.ML_ANTIQ -> COMMENT4,
       Markup.DOC_ANTIQ -> COMMENT4,
       // outer syntax
-      Markup.IDENT -> 0,
+      Markup.IDENT -> NULL,
       Markup.COMMAND -> OPERATOR,
       Markup.KEYWORD -> KEYWORD4,
       Markup.VERBATIM -> COMMENT3,
@@ -83,7 +83,7 @@
       Markup.MALFORMED -> INVALID,
       Markup.STRING -> LITERAL3,
       Markup.ALTSTRING -> LITERAL1
-    ).withDefaultValue(0)
+    ).withDefaultValue(NULL)
   }
 
   def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =