changeset 37373 | 25078ba44436 |
parent 37197 | 953fc4983439 |
child 38150 | 67fc24df3721 |
--- 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) "<ignored>" else "<malformed>" + id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") /* source text */