--- a/src/Pure/Thy/sessions.scala Tue Sep 26 20:54:40 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Tue Sep 26 22:30:54 2017 +0200
@@ -200,16 +200,7 @@
val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
val loaded_files =
if (inlined_files) {
- val pure_files =
- if (is_pure(info.name)) {
- val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
- val files =
- roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
- map(file => info.dir + Path.explode(file))
- roots ::: files
- }
- else Nil
- pure_files ::: thy_deps.loaded_files
+ resources.pure_files(syntax, info.name, info.dir) ::: thy_deps.loaded_files
}
else Nil