diff -r e8990d0e3965 -r 73939a9b70a3 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -103,7 +103,7 @@
 
         val imports =
           header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
-        Document.Node.Header(imports, header.keywords)
+        Document.Node.Header(imports, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
     }