89 def check_thy_reader(qualifier: String, node_name: Document.Node.Name, reader: Reader[Char]) |
89 def check_thy_reader(qualifier: String, node_name: Document.Node.Name, reader: Reader[Char]) |
90 : Document.Node.Header = |
90 : Document.Node.Header = |
91 { |
91 { |
92 if (reader.source.length > 0) { |
92 if (reader.source.length > 0) { |
93 try { |
93 try { |
94 val header = Thy_Header.read(reader).decode_symbols |
94 val header = Thy_Header.read(reader, node_name.node).decode_symbols |
95 |
95 |
96 val base_name = Long_Name.base_name(node_name.theory) |
96 val base_name = Long_Name.base_name(node_name.theory) |
97 val (name, pos) = header.name |
97 val (name, pos) = header.name |
98 if (base_name != name) |
98 if (base_name != name) |
99 error("Bad file name " + Resources.thy_path(Path.basic(base_name)) + |
99 error("Bad file name " + Resources.thy_path(Path.basic(base_name)) + |
100 " for theory " + quote(name) + Position.here(pos)) |
100 " for theory " + quote(name) + Position.here(pos)) |
101 |
101 |
102 val imports = |
102 val imports = |
103 header.imports.map({ case (s, _) => import_name(qualifier, node_name, s) }) |
103 header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) }) |
104 Document.Node.Header(imports, header.keywords, Nil) |
104 Document.Node.Header(imports, header.keywords, Nil) |
105 } |
105 } |
106 catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
106 catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
107 } |
107 } |
108 else Document.Node.no_header |
108 else Document.Node.no_header |