equal
deleted
inserted
replaced
112 if (name.theory != name1) |
112 if (name.theory != name1) |
113 error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + |
113 error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + |
114 " for theory " + quote(name1)) |
114 " for theory " + quote(name1)) |
115 |
115 |
116 val imports = header.imports.map(import_name(name.dir, _)) |
116 val imports = header.imports.map(import_name(name.dir, _)) |
117 val uses = header.uses |
117 Document.Node.Header(imports, header.keywords, Nil) |
118 Document.Node.Header(imports, header.keywords, uses) |
|
119 } |
118 } |
120 catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
119 catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
121 } |
120 } |
122 |
121 |
123 def check_thy(name: Document.Node.Name): Document.Node.Header = |
122 def check_thy(name: Document.Node.Name): Document.Node.Header = |