# HG changeset patch
# User wenzelm
# Date 1237581117 -3600
# Node ID fc851e58a610dc3464adb003cfb26e77d2824ca6
# Parent  909b2610da52f63f2f48ea4170541a06ae56121d
added ML syntax markup;

diff -r 909b2610da52 -r fc851e58a610 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Fri Mar 20 21:31:45 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Fri Mar 20 21:31:57 2009 +0100
@@ -53,6 +53,13 @@
         | Markup.INNER_COMMENT => 5
       case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP
         | Markup.ATTRIBUTE | Markup.METHOD => 6
+      // ML syntax
+      case Markup.ML_KEYWORD | Markup.ML_IDENT => 8
+      case Markup.ML_TVAR => 4
+      case Markup.ML_NUMERAL => 5
+      case Markup.ML_CHAR | Markup.ML_STRING => 13
+      case Markup.ML_COMMENT => 10
+      case Markup.ML_MALFORMED => 12
       // embedded source text
       case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ
         | Markup.DOC_ANTIQ => 7