58 val dir1 = append(dir, path.dir) |
58 val dir1 = append(dir, path.dir) |
59 Document.Node.Name(node, dir1, theory) |
59 Document.Node.Name(node, dir1, theory) |
60 } |
60 } |
61 } |
61 } |
62 |
62 |
63 def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Deps = |
63 def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Header = |
64 { |
64 { |
65 val name1 = header.name |
65 val name1 = header.name |
66 val imports = header.imports.map(import_name(name.dir, _)) |
66 val imports = header.imports.map(import_name(name.dir, _)) |
67 // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2)) |
67 // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2)) |
68 val uses = header.uses |
68 val uses = header.uses |
69 if (name.theory != name1) |
69 if (name.theory != name1) |
70 error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + |
70 error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + |
71 " for theory " + quote(name1)) |
71 " for theory " + quote(name1)) |
72 Document.Node.Deps(imports, header.keywords, uses) |
72 Document.Node.Header(imports, header.keywords, uses) |
73 } |
73 } |
74 |
74 |
75 def check_thy(name: Document.Node.Name): Document.Node.Deps = |
75 def check_thy(name: Document.Node.Name): Document.Node.Header = |
76 check_header(name, read_header(name)) |
76 check_header(name, read_header(name)) |
77 } |
77 } |
78 |
78 |