added ML syntax markup;
authorwenzelm
Fri, 20 Mar 2009 21:31:57 +0100
changeset 34521 fc851e58a610
parent 34520 909b2610da52
child 34542 e647f063ffad
added ML syntax markup;
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