changeset 63020 | 02921dcc42c3 |
parent 62556 | c115e69f457f |
child 63579 | 73939a9b70a3 |
--- 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)) } }