src/Pure/System/build.scala

   type Options = List[(String, Option[String])]
 
   case class Session_Info(
     dir: Path,
     name: String,
-    parent: String,
+    parent: Option[String],
     description: String,
     options: Options,
     theories: List[(Options, String)],
     files: List[String])
-
-  private val pure_info =
-    Session_Info(Path.current, "Pure", "", "", Nil, List((Nil, "Pure")), Nil)
 
 
   /* parsing */
 
   val ROOT_NAME = "ROOT"
 
   private case class Session_Entry(
     name: String,
     reset: Boolean,
     path: Option[String],
-    parent: String,
+    parent: Option[String],
     description: String,
     options: Options,
     theories: List[(Options, List[String])],
     files: List[String])
 

           { case _ ~ (x ~ y) => (x, y) }
 
       ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
         (keyword("!") ^^^ true | success(false)) ~
         (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
-        (keyword("=") ~> session_name <~ keyword("+")) ~
+        (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
         (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
-        rep1(theories) ~
+        rep(theories) ~
         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
           { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) }
     }
 
     def parse_entries(root: File): List[Session_Entry] =

   /* find sessions */
 
   def find_sessions(more_dirs: List[Path]): List[Session_Info] =
   {
     val infos = new mutable.ListBuffer[Session_Info]
-    infos += pure_info
 
     for {
       (dir, strict) <- Isabelle_System.components().map((_, false)) ++ more_dirs.map((_, true))
       root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
       _ = (strict && !root.isFile && error("Bad session root file: " + quote(root.toString)))
       if root.isFile
       entry <- Parser.parse_entries(root)
     }
     {
       try {
-        val parent =
-          infos.find(_.name == entry.parent) getOrElse
-           error("Unknown parent session: " + quote(entry.parent))
+        if (entry.name == "") error("Bad session name")
+
         val full_name =
-          if (entry.reset) entry.name
-          else parent.name + "-" + entry.name
-
-        if (entry.name == "") error("Bad session name")
-        if (infos.exists(_.name == full_name))
-          error("Duplicate session name: " + quote(full_name))
+          if (entry.name == "RAW" || entry.name == "Pure") {
+            if (entry.parent.isDefined) error("Illegal parent session")
+            else entry.name
+          }
+          else
+            entry.parent match {
+              case None => error("Missing parent session")
+              case Some(parent) =>
+                val parent_info =
+                  infos.find(_.name == parent) getOrElse
+                   error("Undefined parent session: " + quote(parent))
+                if (entry.reset) entry.name
+                else parent_info.name + "-" + entry.name
+            }
 
         val path =
           entry.path match {
             case Some(p) => Path.explode(p)
             case None => Path.basic(entry.name)

         val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
         val info =
           Session_Info(dir + path, full_name, entry.parent, entry.description,
             entry.options, thys, entry.files)
 
+        if (infos.exists(_.name == full_name))
+          error("Duplicate session: " + quote(full_name))
         infos += info
       }
       catch {
         case ERROR(msg) =>
           error(msg + "\nThe error(s) above occurred in session entry " +