--- a/src/Pure/PIDE/command.scala Sun May 30 16:54:40 2010 +0200
+++ b/src/Pure/PIDE/command.scala Sun May 30 18:23:50 2010 +0200
@@ -26,7 +26,9 @@
val UNDEFINED = Value("UNDEFINED")
}
- case class HighlightInfo(highlight: String) { override def toString = highlight }
+ case class HighlightInfo(kind: String, sub_kind: Option[String]) {
+ override def toString = kind
+ }
case class TypeInfo(ty: String)
case class RefInfo(file: Option[String], line: Option[Int],
command_id: Option[String], offset: Option[Int])