src/Pure/PIDE/document.scala
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))