src/Pure/PIDE/markup.scala
changeset 55687 78c83cd477c1
parent 55672 5e25cc741ab9
child 55694 a1184dfb8e00
     1.1 --- a/src/Pure/PIDE/markup.scala	Sun Feb 23 10:44:57 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sun Feb 23 14:39:51 2014 +0100
     1.3 @@ -69,6 +69,7 @@
     1.4  
     1.5    /* completion */
     1.6  
     1.7 +  val TOTAL = "total"
     1.8    val COMPLETION = "completion"
     1.9  
    1.10