diff -r 84eb792224a8 -r 34c29356930e src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sat Jul 13 12:39:45 2013 +0200 +++ b/src/Pure/PIDE/markup.scala Sat Jul 13 13:25:42 2013 +0200 @@ -293,6 +293,7 @@ val BAD = "bad" val INTENSIFY = "intensify" + val INFORMATION = "information" /* active areas */