src/Pure/PIDE/protocol.ML
changeset 59934 b65c4370f831
parent 59715 4f0d0e4ad68d
child 60074 38a64cc17403
     1.1 --- a/src/Pure/PIDE/protocol.ML	Mon Apr 06 14:09:31 2015 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Apr 06 16:00:19 2015 +0200
     1.3 @@ -81,7 +81,8 @@
     1.4                                (option (pair (pair string (list string)) (list string)))))
     1.5                                (list YXML.string_of_body)))) a;
     1.6                          val imports' = map (rpair Position.none) imports;
     1.7 -                        val header = Thy_Header.make (name, Position.none) imports' keywords;
     1.8 +                        val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
     1.9 +                        val header = Thy_Header.make (name, Position.none) imports' keywords';
    1.10                        in Document.Deps {master = master, header = header, errors = errors} end,
    1.11                      fn (a :: b, c) =>
    1.12                        Document.Perspective (bool_atom a, map int_atom b,