diff -r babe498016e8 -r 25078ba44436 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri Jun 11 21:58:40 2010 +0200 +++ b/src/Pure/PIDE/command.scala Sun Jun 13 22:33:18 2010 +0200 @@ -48,8 +48,7 @@ def name: String = if (is_command) span.head.content else "" override def toString = - if (is_command) name + "(" + id + ")" - else if (is_ignored) "" else "" + id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") /* source text */