--- a/src/Pure/PIDE/protocol.scala Mon Sep 02 10:41:14 2019 +0200
+++ b/src/Pure/PIDE/protocol.scala Mon Sep 02 11:46:27 2019 +0200
@@ -301,7 +301,7 @@
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
{ case Document.Node.Deps(header) =>
val master_dir = File.standard_url(name.master_dir)
- val imports = header.imports.map({ case (a, _) => a.node })
+ val imports = header.imports.map(_.node)
val keywords =
header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
(Nil,