| changeset 57912 | dd9550f84106 |
| parent 57911 | dcb758188aa6 |
| child 59072 | 27c6936c6484 |
--- a/src/Pure/PIDE/command.scala Tue Aug 12 15:31:24 2014 +0200 +++ b/src/Pure/PIDE/command.scala Tue Aug 12 15:46:20 2014 +0200 @@ -325,7 +325,7 @@ def position: Position.T = span.kind match { case Command_Span.Command_Span(_, pos) => pos case _ => Position.none } - override def toString = id + "/" + span.kind.toString + override def toString: String = id + "/" + span.kind.toString /* classification */