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