src/Pure/Thy/sessions.scala
changeset 62946 9f537dd83677
parent 62944 3ee643c5ed00
child 62968 4e4738698db4
--- a/src/Pure/Thy/sessions.scala	Sun Apr 10 22:27:05 2016 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun Apr 10 22:27:43 2016 +0200
@@ -20,14 +20,12 @@
 
   def pure_name(name: String): Boolean = name == "Pure"
 
-  val pure_roots: List[String] = List("ROOT0.ML", "ROOT.ML")
-
   def pure_files(resources: Resources, syntax: Outer_Syntax, dir: Path): List[Path] =
   {
+    val roots = Thy_Header.ml_roots.map(_._1)
     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))
+      roots.flatMap(root => resources.loaded_files(syntax, File.read(dir + Path.explode(root))))
+    (roots ::: loaded_files).map(file => dir + Path.explode(file))
   }