diff -r b33df9837850 -r bc118a32a870 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Thu Apr 03 19:49:53 2014 +0200 +++ b/src/Pure/Thy/thy_info.scala Thu Apr 03 20:17:12 2014 +0200 @@ -31,12 +31,10 @@ name: Document.Node.Name, header: Document.Node.Header) { - def load_files(syntax: Outer_Syntax): List[String] = + def loaded_files(syntax: Outer_Syntax): List[String] = { val string = resources.with_thy_text(name, _.toString) - if (resources.body_files_test(syntax, string)) - resources.body_files(syntax, string) - else Nil + resources.loaded_files(syntax, string) } } @@ -87,12 +85,12 @@ def loaded_theories: Set[String] = (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory } - def load_files: List[Path] = + def loaded_files: List[Path] = { val dep_files = rev_deps.par.map(dep => Exn.capture { - dep.load_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a)) + dep.loaded_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a)) }).toList ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => Exn.release(files) ::: acc_files