equal
deleted
inserted
replaced
25 /* file-system operations */ |
25 /* file-system operations */ |
26 |
26 |
27 def append(dir: String, source_path: Path): String = |
27 def append(dir: String, source_path: Path): String = |
28 (Path.explode(dir) + source_path).expand.implode |
28 (Path.explode(dir) + source_path).expand.implode |
29 |
29 |
30 def read_header(name: Document.Node.Name): Thy_Header = |
|
31 { |
|
32 val path = Path.explode(name.node) |
|
33 if (!path.is_file) error("No such file: " + path.toString) |
|
34 Thy_Header.read(path.file) |
|
35 } |
|
36 |
|
37 |
30 |
38 /* theory files */ |
31 /* theory files */ |
39 |
32 |
40 private def import_name(dir: String, s: String): Document.Node.Name = |
33 private def import_name(dir: String, s: String): Document.Node.Name = |
41 { |
34 { |
47 val dir1 = append(dir, path.dir) |
40 val dir1 = append(dir, path.dir) |
48 Document.Node.Name(node, dir1, theory) |
41 Document.Node.Name(node, dir1, theory) |
49 } |
42 } |
50 } |
43 } |
51 |
44 |
52 def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Header = |
45 def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = |
53 { |
46 { |
|
47 val header = Thy_Header.read(text) |
54 val name1 = header.name |
48 val name1 = header.name |
55 val imports = header.imports.map(import_name(name.dir, _)) |
49 val imports = header.imports.map(import_name(name.dir, _)) |
56 // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2)) |
50 // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2)) |
57 val uses = header.uses |
51 val uses = header.uses |
58 if (name.theory != name1) |
52 if (name.theory != name1) |
60 " for theory " + quote(name1)) |
54 " for theory " + quote(name1)) |
61 Document.Node.Header(imports, header.keywords, uses) |
55 Document.Node.Header(imports, header.keywords, uses) |
62 } |
56 } |
63 |
57 |
64 def check_thy(name: Document.Node.Name): Document.Node.Header = |
58 def check_thy(name: Document.Node.Name): Document.Node.Header = |
65 check_header(name, read_header(name)) |
59 { |
|
60 val path = Path.explode(name.node) |
|
61 if (!path.is_file) error("No such file: " + path.toString) |
|
62 check_thy_text(name, File.read(path)) |
|
63 } |
66 } |
64 } |
67 |
65 |