# HG changeset patch
# User wenzelm
# Date 1460320063 -7200
# Node ID 9f537dd836772b1825e97a41f956d7bf62b311c1
# Parent  c38c08889aa9ae3718984213cf2d43f2d8f29028
tuned;

diff -r c38c08889aa9 -r 9f537dd83677 src/Pure/Thy/sessions.scala
--- 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))
   }
 
 
diff -r c38c08889aa9 -r 9f537dd83677 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Apr 10 22:27:05 2016 +0200
+++ b/src/Pure/Thy/thy_header.scala	Sun Apr 10 22:27:43 2016 +0200
@@ -69,7 +69,7 @@
   /* file name */
 
   val ML_BOOTSTRAP = "ML_Bootstrap"
-  val ml_roots = Map("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
+  val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
 
   private val Base_Name = new Regex(""".*?([^/\\:]+)""")
   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
@@ -80,7 +80,7 @@
   def thy_name(s: String): Option[String] =
     s match {
       case Thy_Name(name) => Some(name)
-      case Base_Name(name) => ml_roots.get(name)
+      case Base_Name(name) => ml_roots.collectFirst({ case (a, b) if a == name => b })
       case _ => None
     }
 
diff -r c38c08889aa9 -r 9f537dd83677 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Apr 10 22:27:05 2016 +0200
+++ b/src/Pure/Tools/build.scala	Sun Apr 10 22:27:43 2016 +0200
@@ -281,7 +281,9 @@
         val process =
           if (Sessions.pure_name(name)) {
             ML_Process(info.options, raw_ml_system = true, cwd = info.dir.file,
-              args = List("--use", "ROOT0.ML", "--use", "ROOT.ML", "--eval", eval),
+              args =
+                (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
+                List("--eval", eval),
               env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
           }
           else {