src/Pure/PIDE/markup.scala
changeset 56278 2576d3a40ed6
parent 56202 0a11d17eeeff
child 56548 ae6870efc28d
--- 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"