# HG changeset patch
# User wenzelm
# Date 1276461198 -7200
# Node ID 25078ba4443643c8143d279fd703e4dc617aa099
# Parent  babe498016e8a8360dcbaf15846d81d8eee7decc
tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;

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) "<ignored>" else "<malformed>"
+    id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
 
 
   /* source text */