src/Pure/PIDE/protocol.scala
changeset 65384 36255c43c64c
parent 65345 2fdd4431b30e
child 65439 862bfd2b4fd4
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Apr 04 22:53:01 2017 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Apr 04 22:56:28 2017 +0200
     1.3 @@ -361,10 +361,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 =
     1.8 +                header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
     1.9                (Nil,
    1.10                  pair(string, pair(string, pair(list(string), pair(list(pair(string,
    1.11                      pair(pair(string, list(string)), list(string)))), list(string)))))(
    1.12 -                (master_dir, (theory, (imports, (header.keywords, header.errors)))))) },
    1.13 +                (master_dir, (theory, (imports, (keywords, header.errors)))))) },
    1.14            { case Document.Node.Perspective(a, b, c) =>
    1.15                (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
    1.16                  list(pair(id, pair(string, list(string))))(c.dest)) }))