diff -r c4f75e733812 -r 2576d3a40ed6 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Mar 25 15:15:33 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Tue Mar 25 16:11:00 2014 +0100 @@ -101,6 +101,7 @@ object Language { val ML = "ML" + val SML = "SML" val UNKNOWN = "unknown" def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] = @@ -202,6 +203,8 @@ val ML_CHAR = "ML_char" val ML_STRING = "ML_string" val ML_COMMENT = "ML_comment" + val SML_STRING = "SML_string" + val SML_COMMENT = "SML_comment" val ML_DEF = "ML_def" val ML_OPEN = "ML_open"