diff -r 0fb331032f02 -r a50837b637dc src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Aug 12 13:18:17 2014 +0200 +++ b/src/Pure/PIDE/command.scala Tue Aug 12 14:15:58 2014 +0200 @@ -317,13 +317,19 @@ val init_results: Command.Results, val init_markup: Markup_Tree) { - /* name and classification */ + /* name */ def name: String = - span.kind match { case Command_Span.Command_Span(name) => name case _ => "" } + span.kind match { case Command_Span.Command_Span(name, _) => name case _ => "" } + + def position: Position.T = + span.kind match { case Command_Span.Command_Span(_, pos) => pos case _ => Position.none } override def toString = id + "/" + span.kind.toString + + /* classification */ + def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span] def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span