equal
deleted
inserted
replaced
45 /* span kind */ |
45 /* span kind */ |
46 |
46 |
47 sealed abstract class Kind { |
47 sealed abstract class Kind { |
48 override def toString: String = |
48 override def toString: String = |
49 this match { |
49 this match { |
50 case Command_Span(name, _, _) => proper_string(name) getOrElse "<command>" |
50 case Command_Span(name, _) => proper_string(name) getOrElse "<command>" |
51 case Ignored_Span => "<ignored>" |
51 case Ignored_Span => "<ignored>" |
52 case Malformed_Span => "<malformed>" |
52 case Malformed_Span => "<malformed>" |
53 case Theory_Span => "<theory>" |
53 case Theory_Span => "<theory>" |
54 } |
54 } |
55 } |
55 } |
56 case class Command_Span(name: String, pos: Position.T, abs_pos: Position.T) extends Kind |
56 case class Command_Span(name: String, pos: Position.T) extends Kind |
57 case object Ignored_Span extends Kind |
57 case object Ignored_Span extends Kind |
58 case object Malformed_Span extends Kind |
58 case object Malformed_Span extends Kind |
59 case object Theory_Span extends Kind |
59 case object Theory_Span extends Kind |
60 |
60 |
61 |
61 |
68 def name: String = |
68 def name: String = |
69 kind match { case k: Command_Span => k.name case _ => "" } |
69 kind match { case k: Command_Span => k.name case _ => "" } |
70 |
70 |
71 def position: Position.T = |
71 def position: Position.T = |
72 kind match { case k: Command_Span => k.pos case _ => Position.none } |
72 kind match { case k: Command_Span => k.pos case _ => Position.none } |
73 |
|
74 def absolute_position: Position.T = |
|
75 kind match { case k: Command_Span => k.abs_pos case _ => Position.none } |
|
76 |
73 |
77 def keyword_pos(start: Token.Pos): Token.Pos = |
74 def keyword_pos(start: Token.Pos): Token.Pos = |
78 kind match { |
75 kind match { |
79 case _: Command_Span => |
76 case _: Command_Span => |
80 (start /: content.iterator.takeWhile(tok => !tok.is_command))(_.advance(_)) |
77 (start /: content.iterator.takeWhile(tok => !tok.is_command))(_.advance(_)) |