src/Pure/Thy/sessions.scala
changeset 62883 b04e9fe29223
parent 62864 2d5959cf3c1a
child 62902 3c0f53eae166
--- a/src/Pure/Thy/sessions.scala	Tue Apr 05 22:31:28 2016 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Apr 06 11:37:37 2016 +0200
@@ -16,9 +16,17 @@
 
 object Sessions
 {
-  /* info */
+  /* Pure */
+
+  def pure_name(name: String): Boolean = name == "Pure"
+
+  val pure_roots: List[Path] = List("ROOT0.ML", "ROOT.ML", "ROOT1.ML").map(Path.explode(_))
 
-  def is_pure(name: String): Boolean = name == "Pure"
+  def pure_files(dir: Path): List[Path] =
+    (pure_roots ::: pure_roots.flatMap(root => ML_Root.read_files(dir + root))).map(dir + _)
+
+
+  /* info */
 
   sealed case class Info(
     chapter: String,
@@ -221,8 +229,8 @@
           val name = entry.name
 
           if (name == "") error("Bad session name")
-          if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
-          if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
+          if (pure_name(name) && entry.parent.isDefined) error("Illegal parent session")
+          if (!pure_name(name) && !entry.parent.isDefined) error("Missing parent session")
 
           val session_options = options ++ entry.options