src/Pure/PIDE/command.scala
changeset 38355 8cb265fb12fe
parent 38220 b30aa2dbedca
child 38360 53224a4d2f0e
equal deleted inserted replaced
38354:fed4e71a8c0f 38355:8cb265fb12fe
    29   case class HighlightInfo(kind: String, sub_kind: Option[String]) {
    29   case class HighlightInfo(kind: String, sub_kind: Option[String]) {
    30     override def toString = kind
    30     override def toString = kind
    31   }
    31   }
    32   case class TypeInfo(ty: String)
    32   case class TypeInfo(ty: String)
    33   case class RefInfo(file: Option[String], line: Option[Int],
    33   case class RefInfo(file: Option[String], line: Option[Int],
    34     command_id: Option[String], offset: Option[Int])
    34     command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. State_ID !?
    35 }
    35 }
    36 
    36 
    37 class Command(
    37 class Command(
    38     val id: Document.Command_ID,
    38     val id: Document.Command_ID,
    39     val span: Thy_Syntax.Span,
    39     val span: Thy_Syntax.Span,