equal
deleted
inserted
replaced
84 imports_pos: List[(Name, Position.T)] = Nil, |
84 imports_pos: List[(Name, Position.T)] = Nil, |
85 keywords: Thy_Header.Keywords = Nil, |
85 keywords: Thy_Header.Keywords = Nil, |
86 abbrevs: Thy_Header.Abbrevs = Nil, |
86 abbrevs: Thy_Header.Abbrevs = Nil, |
87 errors: List[String] = Nil) |
87 errors: List[String] = Nil) |
88 { |
88 { |
|
89 def imports_offset: Map[Int, Name] = |
|
90 (for { (name, Position.Offset(i)) <- imports_pos } yield i -> name).toMap |
|
91 |
89 def imports: List[Name] = imports_pos.map(_._1) |
92 def imports: List[Name] = imports_pos.map(_._1) |
90 |
93 |
91 def append_errors(msgs: List[String]): Header = |
94 def append_errors(msgs: List[String]): Header = |
92 copy(errors = errors ::: msgs) |
95 copy(errors = errors ::: msgs) |
93 |
96 |