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