--- 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"