211 def parse_change( |
211 def parse_change( |
212 reparse_limit: Int, |
212 reparse_limit: Int, |
213 previous: Document.Version, |
213 previous: Document.Version, |
214 doc_blobs: Document.Blobs, |
214 doc_blobs: Document.Blobs, |
215 edits: List[Document.Edit_Text]): Session.Change = |
215 edits: List[Document.Edit_Text]): Session.Change = |
216 Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits) |
216 Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits) |
217 |
217 |
218 def commit(change: Session.Change) { } |
218 def commit(change: Session.Change) { } |
|
219 |
|
220 |
|
221 /* theory and file dependencies */ |
|
222 |
|
223 object Dependencies |
|
224 { |
|
225 val empty = new Dependencies(Nil, Set.empty) |
|
226 } |
|
227 |
|
228 final class Dependencies private( |
|
229 rev_entries: List[Document.Node.Entry], |
|
230 val seen: Set[Document.Node.Name]) |
|
231 { |
|
232 def :: (entry: Document.Node.Entry): Dependencies = |
|
233 new Dependencies(entry :: rev_entries, seen) |
|
234 |
|
235 def + (name: Document.Node.Name): Dependencies = |
|
236 new Dependencies(rev_entries, seen + name) |
|
237 |
|
238 def entries: List[Document.Node.Entry] = rev_entries.reverse |
|
239 def names: List[Document.Node.Name] = entries.map(_.name) |
|
240 |
|
241 def errors: List[String] = entries.flatMap(_.header.errors) |
|
242 |
|
243 lazy val loaded_theories: Graph[String, Outer_Syntax] = |
|
244 (session_base.loaded_theories /: entries)({ case (graph, entry) => |
|
245 val name = entry.name.theory |
|
246 val imports = entry.header.imports.map(p => p._1.theory) |
|
247 |
|
248 val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty)) |
|
249 val graph2 = (graph1 /: imports)(_.add_edge(_, name)) |
|
250 |
|
251 val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil |
|
252 val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node(_)) |
|
253 val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header |
|
254 |
|
255 graph2.map_node(name, _ => syntax) |
|
256 }) |
|
257 |
|
258 def loaded_files: List[(String, List[Path])] = |
|
259 { |
|
260 names.map(_.theory) zip |
|
261 Par_List.map((e: () => List[Path]) => e(), |
|
262 names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name))) |
|
263 } |
|
264 |
|
265 def imported_files: List[Path] = |
|
266 { |
|
267 val base_theories = |
|
268 loaded_theories.all_preds(names.map(_.theory)). |
|
269 filter(session_base.loaded_theories.defined(_)) |
|
270 |
|
271 base_theories.map(theory => session_base.known.theories(theory).path) ::: |
|
272 base_theories.flatMap(session_base.known.loaded_files(_)) |
|
273 } |
|
274 |
|
275 lazy val overall_syntax: Outer_Syntax = |
|
276 Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_))) |
|
277 |
|
278 override def toString: String = entries.toString |
|
279 } |
|
280 |
|
281 private def show_path(names: List[Document.Node.Name]): String = |
|
282 names.map(name => quote(name.theory)).mkString(" via ") |
|
283 |
|
284 private def cycle_msg(names: List[Document.Node.Name]): String = |
|
285 "Cyclic dependency of " + show_path(names) |
|
286 |
|
287 private def required_by(initiators: List[Document.Node.Name]): String = |
|
288 if (initiators.isEmpty) "" |
|
289 else "\n(required by " + show_path(initiators.reverse) + ")" |
|
290 |
|
291 private def require_thy(initiators: List[Document.Node.Name], required: Dependencies, |
|
292 thy: (Document.Node.Name, Position.T)): Dependencies = |
|
293 { |
|
294 val (name, pos) = thy |
|
295 |
|
296 def message: String = |
|
297 "The error(s) above occurred for theory " + quote(name.theory) + |
|
298 required_by(initiators) + Position.here(pos) |
|
299 |
|
300 val required1 = required + name |
|
301 if (required.seen(name)) required |
|
302 else if (session_base.loaded_theory(name)) required1 |
|
303 else { |
|
304 try { |
|
305 if (initiators.contains(name)) error(cycle_msg(initiators)) |
|
306 val header = |
|
307 try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) } |
|
308 catch { case ERROR(msg) => cat_error(msg, message) } |
|
309 Document.Node.Entry(name, header) :: |
|
310 require_thys(name :: initiators, required1, header.imports) |
|
311 } |
|
312 catch { |
|
313 case e: Throwable => |
|
314 Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1 |
|
315 } |
|
316 } |
|
317 } |
|
318 |
|
319 private def require_thys(initiators: List[Document.Node.Name], required: Dependencies, |
|
320 thys: List[(Document.Node.Name, Position.T)]): Dependencies = |
|
321 (required /: thys)(require_thy(initiators, _, _)) |
|
322 |
|
323 def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies = |
|
324 require_thys(Nil, Dependencies.empty, thys) |
219 } |
325 } |