changeset 63579 | 73939a9b70a3 |
parent 63032 | e0fa59bbc956 |
child 63584 | 68751fe1c036 |
--- a/src/Pure/PIDE/document.scala Tue Aug 02 11:49:30 2016 +0200 +++ b/src/Pure/PIDE/document.scala Tue Aug 02 17:35:18 2016 +0200 @@ -83,6 +83,7 @@ sealed case class Header( imports: List[(Name, Position.T)] = Nil, keywords: Thy_Header.Keywords = Nil, + abbrevs: Thy_Header.Abbrevs = Nil, errors: List[String] = Nil) { def error(msg: String): Header = copy(errors = errors ::: List(msg))