src/Pure/PIDE/protocol.ML
changeset 48927 ef462b5558eb
parent 48864 3ee314ae1e0a
child 49061 7449b804073b
     1.1 --- a/src/Pure/PIDE/protocol.ML	Sun Aug 26 10:20:26 2012 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Sun Aug 26 21:46:50 2012 +0200
     1.3 @@ -42,10 +42,11 @@
     1.4                            (pair (list (pair string
     1.5                              (option (pair (pair string (list string)) (list string)))))
     1.6                              (pair (list (pair string bool)) (list string))))) a;
     1.7 +                      val imports' = map (rpair Position.none) imports;
     1.8                        val (uses', errors') =
     1.9                          (map (apfst Path.explode) uses, errors)
    1.10                            handle ERROR msg => ([], errors @ [msg]);
    1.11 -                      val header = Thy_Header.make name imports keywords uses';
    1.12 +                      val header = Thy_Header.make (name, Position.none) imports' keywords uses';
    1.13                      in Document.Deps (master, header, errors') end,
    1.14                    fn (a, []) => Document.Perspective (map int_atom a)]))
    1.15              end;