--- a/src/Pure/PIDE/command.scala Sun Aug 22 13:59:47 2010 +0200
+++ b/src/Pure/PIDE/command.scala Sun Aug 22 16:37:15 2010 +0200
@@ -14,11 +14,6 @@
object Command
{
- case class RefInfo(file: Option[String], line: Option[Int],
- command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. Exec_ID !?
-
-
-
/** accumulated results from prover **/
case class State(
@@ -40,17 +35,6 @@
def markup_root: Markup_Tree = markup + markup_root_node
- /* markup */
-
- private lazy val refs: List[Markup_Tree.Node[Any]] =
- markup.filter(_.info match {
- case Command.RefInfo(_, _, _, _) => true
- case _ => false }).flatten(markup_root_node)
-
- def ref_at(pos: Text.Offset): Option[Markup_Tree.Node[Any]] =
- refs.find(_.range.contains(pos))
-
-
/* message dispatch */
def accumulate(message: XML.Tree): Command.State =