src/Pure/PIDE/protocol.scala
changeset 63579 73939a9b70a3
parent 63429 baedd4724f08
child 63805 c272680df665
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Aug 02 11:49:30 2016 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Aug 02 17:35:18 2016 +0200
     1.3 @@ -374,13 +374,12 @@
     1.4                val master_dir = File.standard_url(name.master_dir)
     1.5                val theory = Long_Name.base_name(name.theory)
     1.6                val imports = header.imports.map({ case (a, _) => a.node })
     1.7 -              val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
     1.8                (Nil,
     1.9                  pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
    1.10                    pair(list(pair(Encode.string,
    1.11                      pair(pair(Encode.string, list(Encode.string)), list(Encode.string)))),
    1.12                    list(Encode.string)))))(
    1.13 -                (master_dir, (theory, (imports, (keywords, header.errors)))))) },
    1.14 +                (master_dir, (theory, (imports, (header.keywords, header.errors)))))) },
    1.15            { case Document.Node.Perspective(a, b, c) =>
    1.16                (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
    1.17                  list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))