diff -r e8990d0e3965 -r 73939a9b70a3 src/Pure/PIDE/document.scala --- 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))