src/Pure/PIDE/markup.scala
changeset 63347 e344dc82f6c2
parent 63337 ae9330fdbc16
child 63474 f66e3c3b0fb1
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed Jun 22 11:10:18 2016 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jun 22 16:04:03 2016 +0200
     1.3 @@ -267,6 +267,7 @@
     1.4  
     1.5    val SORTING = "sorting"
     1.6    val TYPING = "typing"
     1.7 +  val CLASS_PARAMETER = "class_parameter"
     1.8  
     1.9    val ATTRIBUTE = "attribute"
    1.10    val METHOD = "method"