src/Pure/PIDE/command.scala
changeset 38574 79cb7b4c908a
parent 38572 0fe2c01ef7da
child 38575 80d962964216
     1.1 --- a/src/Pure/PIDE/command.scala	Sun Aug 22 13:52:24 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sun Aug 22 13:59:47 2010 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4  
     1.5  object Command
     1.6  {
     1.7 -  case class TypeInfo(ty: String)
     1.8    case class RefInfo(file: Option[String], line: Option[Int],
     1.9      command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. Exec_ID !?
    1.10  
    1.11 @@ -43,23 +42,6 @@
    1.12  
    1.13      /* markup */
    1.14  
    1.15 -    private lazy val types: List[Markup_Tree.Node[Any]] =
    1.16 -      markup.filter(_.info match {
    1.17 -        case Command.TypeInfo(_) => true
    1.18 -        case _ => false }).flatten(markup_root_node)
    1.19 -
    1.20 -    def type_at(pos: Text.Offset): Option[String] =
    1.21 -    {
    1.22 -      types.find(_.range.contains(pos)) match {
    1.23 -        case Some(t) =>
    1.24 -          t.info match {
    1.25 -            case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
    1.26 -            case _ => None
    1.27 -          }
    1.28 -        case None => None
    1.29 -      }
    1.30 -    }
    1.31 -
    1.32      private lazy val refs: List[Markup_Tree.Node[Any]] =
    1.33        markup.filter(_.info match {
    1.34          case Command.RefInfo(_, _, _, _) => true