equal
deleted
inserted
replaced
96 def import_name(node_name: Document.Node.Name, s: String): Document.Node.Name = |
96 def import_name(node_name: Document.Node.Name, s: String): Document.Node.Name = |
97 import_name(theory_qualifier(node_name), node_name.master_dir, s) |
97 import_name(theory_qualifier(node_name), node_name.master_dir, s) |
98 |
98 |
99 def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
99 def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
100 { |
100 { |
101 val path = Path.explode(name.node) |
101 val path = File.check_file(Path.explode(name.node)) |
102 if (!path.is_file) error("No such file: " + path.toString) |
|
103 |
|
104 val reader = Scan.byte_reader(path.file) |
102 val reader = Scan.byte_reader(path.file) |
105 try { f(reader) } finally { reader.close } |
103 try { f(reader) } finally { reader.close } |
106 } |
104 } |
107 |
105 |
108 def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char], |
106 def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char], |