40 val dir1 = append(dir, path.dir) |
40 val dir1 = append(dir, path.dir) |
41 Document.Node.Name(node, dir1, theory) |
41 Document.Node.Name(node, dir1, theory) |
42 } |
42 } |
43 } |
43 } |
44 |
44 |
45 def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = |
45 def check_thy_text(syntax: Outer_Syntax, name: Document.Node.Name, text: CharSequence) |
|
46 : Document.Node.Header = |
46 { |
47 { |
47 val header = Thy_Header.read(text) |
48 val header = Thy_Header.read(text) |
48 val name1 = header.name |
49 val name1 = header.name |
49 val imports = header.imports.map(import_name(name.dir, _)) |
50 val imports = header.imports.map(import_name(name.dir, _)) |
50 // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2)) |
51 // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2)) |
|
52 // FIXME find files in text |
51 val uses = header.uses |
53 val uses = header.uses |
52 if (name.theory != name1) |
54 if (name.theory != name1) |
53 error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + |
55 error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + |
54 " for theory " + quote(name1)) |
56 " for theory " + quote(name1)) |
55 Document.Node.Header(imports, header.keywords, uses) |
57 Document.Node.Header(imports, header.keywords, uses) |
56 } |
58 } |
57 |
59 |
58 def check_thy(name: Document.Node.Name): Document.Node.Header = |
60 def check_thy(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header = |
59 { |
61 { |
60 val path = Path.explode(name.node) |
62 val path = Path.explode(name.node) |
61 if (!path.is_file) error("No such file: " + path.toString) |
63 if (!path.is_file) error("No such file: " + path.toString) |
62 check_thy_text(name, File.read(path)) |
64 check_thy_text(syntax, name, File.read(path)) |
63 } |
65 } |
64 } |
66 } |
65 |
67 |