# HG changeset patch
# User wenzelm
# Date 1407789806 -7200
# Node ID 3f1fd41ee8210fee9c495f7d286f9d4fd2202051
# Parent  e1abca2527da3216fbe35dfe5869397bd0c257bf
tuned output, in accordance to transaction name in ML;

diff -r e1abca2527da -r 3f1fd41ee821 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Aug 11 22:29:48 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Aug 11 22:43:26 2014 +0200
@@ -325,13 +325,11 @@
 
   def is_command: Boolean = span.kind.isInstanceOf[Thy_Syntax.Command_Span]
   def is_ignored: Boolean = span.kind == Thy_Syntax.Ignored_Span
-  def is_malformed: Boolean = span.kind == Thy_Syntax.Malformed_Span
 
   def name: String =
     span.kind match { case Thy_Syntax.Command_Span(name) => name case _ => "" }
 
-  override def toString =
-    id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
+  override def toString = id + "/" + span.kind.toString
 
 
   /* blobs */
diff -r e1abca2527da -r 3f1fd41ee821 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 22:29:48 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 22:43:26 2014 +0200
@@ -15,7 +15,14 @@
 {
   /** spans **/
 
-  sealed abstract class Span_Kind
+  sealed abstract class Span_Kind {
+    override def toString: String =
+      this match {
+        case Command_Span(name) => if (name != "") name else "<command>"
+        case Ignored_Span => "<ignored>"
+        case Malformed_Span => "<malformed>"
+      }
+  }
   case class Command_Span(name: String) extends Span_Kind
   case object Ignored_Span extends Span_Kind
   case object Malformed_Span extends Span_Kind