tuned output, in accordance to transaction name in ML;
authorwenzelm
Mon Aug 11 22:43:26 2014 +0200 (2014-08-11 ago)
changeset 579023f1fd41ee821
parent 57901 e1abca2527da
child 57903 ade8d65b212e
tuned output, in accordance to transaction name in ML;
src/Pure/PIDE/command.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Mon Aug 11 22:29:48 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Mon Aug 11 22:43:26 2014 +0200
     1.3 @@ -325,13 +325,11 @@
     1.4  
     1.5    def is_command: Boolean = span.kind.isInstanceOf[Thy_Syntax.Command_Span]
     1.6    def is_ignored: Boolean = span.kind == Thy_Syntax.Ignored_Span
     1.7 -  def is_malformed: Boolean = span.kind == Thy_Syntax.Malformed_Span
     1.8  
     1.9    def name: String =
    1.10      span.kind match { case Thy_Syntax.Command_Span(name) => name case _ => "" }
    1.11  
    1.12 -  override def toString =
    1.13 -    id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
    1.14 +  override def toString = id + "/" + span.kind.toString
    1.15  
    1.16  
    1.17    /* blobs */
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 22:29:48 2014 +0200
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 22:43:26 2014 +0200
     2.3 @@ -15,7 +15,14 @@
     2.4  {
     2.5    /** spans **/
     2.6  
     2.7 -  sealed abstract class Span_Kind
     2.8 +  sealed abstract class Span_Kind {
     2.9 +    override def toString: String =
    2.10 +      this match {
    2.11 +        case Command_Span(name) => if (name != "") name else "<command>"
    2.12 +        case Ignored_Span => "<ignored>"
    2.13 +        case Malformed_Span => "<malformed>"
    2.14 +      }
    2.15 +  }
    2.16    case class Command_Span(name: String) extends Span_Kind
    2.17    case object Ignored_Span extends Span_Kind
    2.18    case object Malformed_Span extends Span_Kind