13 import java.io.{File => JFile} |
13 import java.io.{File => JFile} |
14 |
14 |
15 |
15 |
16 class Resources( |
16 class Resources( |
17 val session_base: Sessions.Base, |
17 val session_base: Sessions.Base, |
18 val default_qualifier: String = "", |
18 val default_qualifier: String = Sessions.DRAFT, |
19 val log: Logger = No_Logger) |
19 val log: Logger = No_Logger) |
20 { |
20 { |
21 val thy_info = new Thy_Info(this) |
21 val thy_info = new Thy_Info(this) |
22 |
22 |
23 def thy_path(path: Path): Path = path.ext("thy") |
23 def thy_path(path: Path): Path = path.ext("thy") |
65 val spans = syntax.parse_spans(text) |
65 val spans = syntax.parse_spans(text) |
66 spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList |
66 spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList |
67 } |
67 } |
68 else Nil |
68 else Nil |
69 |
69 |
70 def import_name(dir: String, s: String): Document.Node.Name = |
70 def theory_qualifier(name: Document.Node.Name): String = |
|
71 Long_Name.qualifier(name.theory) |
|
72 |
|
73 def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = |
71 { |
74 { |
72 val theory0 = Thy_Header.base_name(s) |
75 val theory0 = Thy_Header.base_name(s) |
73 val theory = |
76 val theory = |
74 if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0 |
77 if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0) |
75 else Long_Name.qualify(default_qualifier, theory0) |
78 || true /* FIXME */) theory0 |
|
79 else theory0 // FIXME Long_Name.qualify(qualifier, theory0) |
76 |
80 |
77 session_base.loaded_theories.get(theory) orElse |
81 session_base.loaded_theories.get(theory) orElse |
78 session_base.loaded_theories.get(theory0) orElse |
82 session_base.loaded_theories.get(theory0) orElse |
79 session_base.known_theories.get(theory) orElse |
83 session_base.known_theories.get(theory) orElse |
80 session_base.known_theories.get(theory0) getOrElse { |
84 session_base.known_theories.get(theory0) getOrElse { |
107 error("Bad theory name " + quote(name) + |
111 error("Bad theory name " + quote(name) + |
108 " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) + |
112 " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) + |
109 Completion.report_names(pos, 1, List((base_name, ("theory", base_name))))) |
113 Completion.report_names(pos, 1, List((base_name, ("theory", base_name))))) |
110 |
114 |
111 val imports = |
115 val imports = |
112 header.imports.map({ case (s, pos) => (import_name(node_name.master_dir, s), pos) }) |
116 header.imports.map({ case (s, pos) => |
|
117 (import_name(theory_qualifier(node_name), node_name.master_dir, s), pos) }) |
113 Document.Node.Header(imports, header.keywords, header.abbrevs) |
118 Document.Node.Header(imports, header.keywords, header.abbrevs) |
114 } |
119 } |
115 catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
120 catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
116 } |
121 } |
117 else Document.Node.no_header |
122 else Document.Node.no_header |
123 |
128 |
124 |
129 |
125 /* special header */ |
130 /* special header */ |
126 |
131 |
127 def special_header(name: Document.Node.Name): Option[Document.Node.Header] = |
132 def special_header(name: Document.Node.Name): Option[Document.Node.Header] = |
128 if (Thy_Header.is_ml_root(name.theory)) |
133 { |
129 Some(Document.Node.Header( |
134 val qualifier = theory_qualifier(name) |
130 List((import_name(name.master_dir, Thy_Header.ML_BOOTSTRAP), Position.none)))) |
135 val dir = name.master_dir |
131 else if (Thy_Header.is_bootstrap(name.theory)) |
136 |
132 Some(Document.Node.Header( |
137 val imports = |
133 List((import_name(name.master_dir, Thy_Header.PURE), Position.none)))) |
138 if (Thy_Header.is_ml_root(name.theory)) |
134 else None |
139 List(import_name(qualifier, dir, Thy_Header.ML_BOOTSTRAP)) |
|
140 else if (Thy_Header.is_bootstrap(name.theory)) |
|
141 List(import_name(qualifier, dir, Thy_Header.PURE)) |
|
142 else Nil |
|
143 |
|
144 if (imports.isEmpty) None |
|
145 else Some(Document.Node.Header(imports.map((_, Position.none)))) |
|
146 } |
135 |
147 |
136 |
148 |
137 /* blobs */ |
149 /* blobs */ |
138 |
150 |
139 def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] = |
151 def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] = |