diff -r ff0b52a6d72f -r 599c935aac82 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Mon Nov 19 20:47:13 2012 +0100 +++ b/src/Pure/PIDE/protocol.scala Mon Nov 19 22:34:17 2012 +0100 @@ -237,6 +237,7 @@ { case Document.Node.Deps(header) => val dir = Isabelle_System.posix_path(name.dir) val imports = header.imports.map(_.node) + val keywords = header.keywords.map({ case (a, b, _) => (a, b) }) // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2)) val uses = header.uses (Nil, @@ -244,7 +245,7 @@ pair(list(pair(Encode.string, option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))), pair(list(pair(Encode.string, bool)), list(Encode.string))))))( - (dir, (name.theory, (imports, (header.keywords, (uses, header.errors))))))) }, + (dir, (name.theory, (imports, (keywords, (uses, header.errors))))))) }, { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => {