src/Pure/PIDE/markup.scala
changeset 55033 8e8243975860
parent 54702 3daeba5130f0
child 55316 885500f4aa6a
     1.1 --- a/src/Pure/PIDE/markup.scala	Fri Jan 17 20:51:36 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sat Jan 18 19:15:12 2014 +0100
     1.3 @@ -133,6 +133,7 @@
     1.4    val LITERAL = "literal"
     1.5    val DELIMITER = "delimiter"
     1.6    val INNER_STRING = "inner_string"
     1.7 +  val INNER_CARTOUCHE = "inner_cartouche"
     1.8    val INNER_COMMENT = "inner_comment"
     1.9  
    1.10    val TOKEN_RANGE = "token_range"
    1.11 @@ -190,6 +191,7 @@
    1.12    val STRING = "string"
    1.13    val ALTSTRING = "altstring"
    1.14    val VERBATIM = "verbatim"
    1.15 +  val CARTOUCHE = "cartouche"
    1.16    val COMMENT = "comment"
    1.17    val CONTROL = "control"
    1.18