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