--- 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 */