--- 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))
}
--- 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
}
--- 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 {