# HG changeset patch
# User wenzelm
# Date 1461005017 -7200
# Node ID 02921dcc42c3191ec20f05ec44fe95fb0d96ffc2
# Parent  80ef19b5149313340b5efae35e65467a5bc618a3
tuned signature;

diff -r 80ef19b51493 -r 02921dcc42c3 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Apr 18 20:24:19 2016 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Apr 18 20:43:37 2016 +0200
@@ -81,9 +81,9 @@
     /* header and name */
 
     sealed case class Header(
-      imports: List[(Name, Position.T)],
-      keywords: Thy_Header.Keywords,
-      errors: List[String])
+      imports: List[(Name, Position.T)] = Nil,
+      keywords: Thy_Header.Keywords = Nil,
+      errors: List[String] = Nil)
     {
       def error(msg: String): Header = copy(errors = errors ::: List(msg))
 
@@ -91,8 +91,8 @@
         copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2)))
     }
 
-    val no_header = Header(Nil, Nil, Nil)
-    def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
+    val no_header = Header()
+    def bad_header(msg: String): Header = Header(errors = List(msg))
 
     object Name
     {
diff -r 80ef19b51493 -r 02921dcc42c3 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Apr 18 20:24:19 2016 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 18 20:43:37 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, Nil)
+        Document.Node.Header(imports, header.keywords)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
     }