src/Pure/PIDE/markup.scala
changeset 56278 2576d3a40ed6
parent 56202 0a11d17eeeff
child 56548 ae6870efc28d
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Mar 25 15:15:33 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Mar 25 16:11:00 2014 +0100
     1.3 @@ -101,6 +101,7 @@
     1.4    object Language
     1.5    {
     1.6      val ML = "ML"
     1.7 +    val SML = "SML"
     1.8      val UNKNOWN = "unknown"
     1.9  
    1.10      def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
    1.11 @@ -202,6 +203,8 @@
    1.12    val ML_CHAR = "ML_char"
    1.13    val ML_STRING = "ML_string"
    1.14    val ML_COMMENT = "ML_comment"
    1.15 +  val SML_STRING = "SML_string"
    1.16 +  val SML_COMMENT = "SML_comment"
    1.17  
    1.18    val ML_DEF = "ML_def"
    1.19    val ML_OPEN = "ML_open"