src/Pure/PIDE/command.scala
changeset 38575 80d962964216
parent 38574 79cb7b4c908a
child 38577 4e4d3ea3725a
     1.1 --- a/src/Pure/PIDE/command.scala	Sun Aug 22 13:59:47 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sun Aug 22 16:37:15 2010 +0200
     1.3 @@ -14,11 +14,6 @@
     1.4  
     1.5  object Command
     1.6  {
     1.7 -  case class RefInfo(file: Option[String], line: Option[Int],
     1.8 -    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. Exec_ID !?
     1.9 -
    1.10 -
    1.11 -
    1.12    /** accumulated results from prover **/
    1.13  
    1.14    case class State(
    1.15 @@ -40,17 +35,6 @@
    1.16      def markup_root: Markup_Tree = markup + markup_root_node
    1.17  
    1.18  
    1.19 -    /* markup */
    1.20 -
    1.21 -    private lazy val refs: List[Markup_Tree.Node[Any]] =
    1.22 -      markup.filter(_.info match {
    1.23 -        case Command.RefInfo(_, _, _, _) => true
    1.24 -        case _ => false }).flatten(markup_root_node)
    1.25 -
    1.26 -    def ref_at(pos: Text.Offset): Option[Markup_Tree.Node[Any]] =
    1.27 -      refs.find(_.range.contains(pos))
    1.28 -
    1.29 -
    1.30      /* message dispatch */
    1.31  
    1.32      def accumulate(message: XML.Tree): Command.State =