src/Pure/Thy/thy_syntax.scala
changeset 57902 3f1fd41ee821
parent 57901 e1abca2527da
child 57904 922273b7bf8a
equal deleted inserted replaced
57901:e1abca2527da 57902:3f1fd41ee821
    13 
    13 
    14 object Thy_Syntax
    14 object Thy_Syntax
    15 {
    15 {
    16   /** spans **/
    16   /** spans **/
    17 
    17 
    18   sealed abstract class Span_Kind
    18   sealed abstract class Span_Kind {
       
    19     override def toString: String =
       
    20       this match {
       
    21         case Command_Span(name) => if (name != "") name else "<command>"
       
    22         case Ignored_Span => "<ignored>"
       
    23         case Malformed_Span => "<malformed>"
       
    24       }
       
    25   }
    19   case class Command_Span(name: String) extends Span_Kind
    26   case class Command_Span(name: String) extends Span_Kind
    20   case object Ignored_Span extends Span_Kind
    27   case object Ignored_Span extends Span_Kind
    21   case object Malformed_Span extends Span_Kind
    28   case object Malformed_Span extends Span_Kind
    22 
    29 
    23   sealed case class Span(kind: Span_Kind, content: List[Token])
    30   sealed case class Span(kind: Span_Kind, content: List[Token])