src/Pure/PIDE/command.scala
changeset 38355 8cb265fb12fe
parent 38220 b30aa2dbedca
child 38360 53224a4d2f0e
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Aug 11 18:44:06 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Wed Aug 11 22:41:26 2010 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4    }
     1.5    case class TypeInfo(ty: String)
     1.6    case class RefInfo(file: Option[String], line: Option[Int],
     1.7 -    command_id: Option[String], offset: Option[Int])
     1.8 +    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. State_ID !?
     1.9  }
    1.10  
    1.11  class Command(