src/Pure/PIDE/command.scala
changeset 50540 f4aac67a6405
parent 50508 5b7150395568
child 51048 123be08eed88
     1.1 --- a/src/Pure/PIDE/command.scala	Fri Dec 14 21:50:21 2012 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Fri Dec 14 23:04:35 2012 +0100
     1.3 @@ -39,6 +39,8 @@
     1.4        if (this eq other) this
     1.5        else if (rep.isEmpty) other
     1.6        else (this /: other.entries)(_ + _)
     1.7 +
     1.8 +    override def toString: String = entries.mkString("Results(", ", ", ")")
     1.9    }
    1.10  
    1.11