src/Pure/Thy/sessions.scala
changeset 66696 8f863dae78a0
parent 66694 41177b124067
child 66701 d181f8a0e857
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Sep 26 20:54:40 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Sep 26 22:30:54 2017 +0200
     1.3 @@ -200,16 +200,7 @@
     1.4              val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
     1.5              val loaded_files =
     1.6                if (inlined_files) {
     1.7 -                val pure_files =
     1.8 -                  if (is_pure(info.name)) {
     1.9 -                    val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
    1.10 -                    val files =
    1.11 -                      roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
    1.12 -                        map(file => info.dir + Path.explode(file))
    1.13 -                    roots ::: files
    1.14 -                  }
    1.15 -                  else Nil
    1.16 -                pure_files ::: thy_deps.loaded_files
    1.17 +                resources.pure_files(syntax, info.name, info.dir) ::: thy_deps.loaded_files
    1.18                }
    1.19                else Nil
    1.20