295 |
295 |
296 private def required_by(initiators: List[Document.Node.Name]): String = |
296 private def required_by(initiators: List[Document.Node.Name]): String = |
297 if (initiators.isEmpty) "" |
297 if (initiators.isEmpty) "" |
298 else "\n(required by " + show_path(initiators.reverse) + ")" |
298 else "\n(required by " + show_path(initiators.reverse) + ")" |
299 |
299 |
300 private def require_thy(initiators: List[Document.Node.Name], required: Dependencies, |
300 private def require_thy( |
|
301 progress: Progress, |
|
302 initiators: List[Document.Node.Name], |
|
303 required: Dependencies, |
301 thy: (Document.Node.Name, Position.T)): Dependencies = |
304 thy: (Document.Node.Name, Position.T)): Dependencies = |
302 { |
305 { |
303 val (name, pos) = thy |
306 val (name, pos) = thy |
304 |
307 |
305 def message: String = |
308 def message: String = |
311 val required1 = required + name |
314 val required1 = required + name |
312 if (session_base.loaded_theory(name)) required1 |
315 if (session_base.loaded_theory(name)) required1 |
313 else { |
316 else { |
314 try { |
317 try { |
315 if (initiators.contains(name)) error(cycle_msg(initiators)) |
318 if (initiators.contains(name)) error(cycle_msg(initiators)) |
|
319 |
|
320 progress.expose_interrupt() |
316 val header = |
321 val header = |
317 try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) } |
322 try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) } |
318 catch { case ERROR(msg) => cat_error(msg, message) } |
323 catch { case ERROR(msg) => cat_error(msg, message) } |
319 Document.Node.Entry(name, header) :: |
324 Document.Node.Entry(name, header) :: |
320 require_thys(name :: initiators, required1, header.imports) |
325 require_thys(progress, name :: initiators, required1, header.imports) |
321 } |
326 } |
322 catch { |
327 catch { |
323 case e: Throwable => |
328 case e: Throwable => |
324 Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1 |
329 Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1 |
325 } |
330 } |
326 } |
331 } |
327 } |
332 } |
328 } |
333 } |
329 |
334 |
330 private def require_thys(initiators: List[Document.Node.Name], required: Dependencies, |
335 private def require_thys( |
|
336 progress: Progress, |
|
337 initiators: List[Document.Node.Name], |
|
338 required: Dependencies, |
331 thys: List[(Document.Node.Name, Position.T)]): Dependencies = |
339 thys: List[(Document.Node.Name, Position.T)]): Dependencies = |
332 (required /: thys)(require_thy(initiators, _, _)) |
340 (required /: thys)(require_thy(progress, initiators, _, _)) |
333 |
341 |
334 def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies = |
342 def dependencies( |
335 require_thys(Nil, Dependencies.empty, thys) |
343 thys: List[(Document.Node.Name, Position.T)], |
|
344 progress: Progress = No_Progress): Dependencies = |
|
345 require_thys(progress, Nil, Dependencies.empty, thys) |
336 } |
346 } |