src/Pure/PIDE/command.scala
changeset 37197 953fc4983439
parent 37189 2b4e52ecf6fc
child 37373 25078ba44436
--- 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])