--- a/src/Pure/PIDE/protocol.ML Tue Feb 26 20:11:11 2013 +0100
+++ b/src/Pure/PIDE/protocol.ML Wed Feb 27 12:45:19 2013 +0100
@@ -37,16 +37,16 @@
fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
fn ([], a) =>
let
- val (master, (name, (imports, (keywords, (uses, errors))))) =
+ val (master, (name, (imports, (keywords, (files, errors))))) =
pair string (pair string (pair (list string)
(pair (list (pair string
(option (pair (pair string (list string)) (list string)))))
- (pair (list (pair string bool)) (list string))))) a;
+ (pair (list string) (list string))))) a;
val imports' = map (rpair Position.none) imports;
- val (uses', errors') =
- (map (apfst Path.explode) uses, errors)
+ val (files', errors') =
+ (map Path.explode files, errors)
handle ERROR msg => ([], errors @ [msg]);
- val header = Thy_Header.make (name, Position.none) imports' keywords uses';
+ val header = Thy_Header.make (name, Position.none) imports' keywords files';
in Document.Deps (master, header, errors') end,
fn (a, []) => Document.Perspective (map int_atom a)]))
end;