src/Pure/Thy/sessions.scala
changeset 62902 3c0f53eae166
parent 62883 b04e9fe29223
child 62944 3ee643c5ed00
--- a/src/Pure/Thy/sessions.scala	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Apr 07 16:53:43 2016 +0200
@@ -20,10 +20,15 @@
 
   def pure_name(name: String): Boolean = name == "Pure"
 
-  val pure_roots: List[Path] = List("ROOT0.ML", "ROOT.ML", "ROOT1.ML").map(Path.explode(_))
+  val pure_roots: List[String] = List("ROOT0.ML", "ROOT.ML", "ROOT1.ML")
 
-  def pure_files(dir: Path): List[Path] =
-    (pure_roots ::: pure_roots.flatMap(root => ML_Root.read_files(dir + root))).map(dir + _)
+  def pure_files(resources: Resources, syntax: Outer_Syntax, dir: Path): List[Path] =
+  {
+    val loaded_files =
+      pure_roots.flatMap(root =>
+        resources.loaded_files(syntax, File.read(dir + Path.explode(root))))
+    (pure_roots ::: loaded_files).map(file => dir + Path.explode(file))
+  }
 
 
   /* info */