equal
deleted
inserted
replaced
81 /* header and name */ |
81 /* header and name */ |
82 |
82 |
83 sealed case class Header( |
83 sealed case class Header( |
84 imports: List[(Name, Position.T)] = Nil, |
84 imports: List[(Name, Position.T)] = Nil, |
85 keywords: Thy_Header.Keywords = Nil, |
85 keywords: Thy_Header.Keywords = Nil, |
|
86 abbrevs: Thy_Header.Abbrevs = Nil, |
86 errors: List[String] = Nil) |
87 errors: List[String] = Nil) |
87 { |
88 { |
88 def error(msg: String): Header = copy(errors = errors ::: List(msg)) |
89 def error(msg: String): Header = copy(errors = errors ::: List(msg)) |
89 |
90 |
90 def cat_errors(msg2: String): Header = |
91 def cat_errors(msg2: String): Header = |