equal
deleted
inserted
replaced
101 " for file " + Resources.thy_path(Path.basic(base_name)) + Position.here(pos) + |
101 " for file " + Resources.thy_path(Path.basic(base_name)) + Position.here(pos) + |
102 Completion.report_names(pos, 1, List((base_name, ("theory", base_name))))) |
102 Completion.report_names(pos, 1, List((base_name, ("theory", base_name))))) |
103 |
103 |
104 val imports = |
104 val imports = |
105 header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) }) |
105 header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) }) |
106 Document.Node.Header(imports, header.keywords, Nil) |
106 Document.Node.Header(imports, header.keywords) |
107 } |
107 } |
108 catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
108 catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
109 } |
109 } |
110 else Document.Node.no_header |
110 else Document.Node.no_header |
111 } |
111 } |