equal
deleted
inserted
replaced
13 object Command_Span |
13 object Command_Span |
14 { |
14 { |
15 sealed abstract class Kind { |
15 sealed abstract class Kind { |
16 override def toString: String = |
16 override def toString: String = |
17 this match { |
17 this match { |
18 case Command_Span(name, _) => if (name != "") name else "<command>" |
18 case Command_Span(name, _) => proper_string(name) getOrElse "<command>" |
19 case Ignored_Span => "<ignored>" |
19 case Ignored_Span => "<ignored>" |
20 case Malformed_Span => "<malformed>" |
20 case Malformed_Span => "<malformed>" |
21 } |
21 } |
22 } |
22 } |
23 case class Command_Span(name: String, pos: Position.T) extends Kind |
23 case class Command_Span(name: String, pos: Position.T) extends Kind |