# HG changeset patch
# User wenzelm
# Date 1342624658 -7200
# Node ID 9c7f8e5805b40b2d546da30e144cbea7813565db
# Parent  3c55bfad22ebdec65f590d8a8b06a9d2f9d25a18
cumulate semantic Session_Info, based on syntactic Session_Entry;
tuned errors;

diff -r 3c55bfad22eb -r 9c7f8e5805b4 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Wed Jul 18 16:24:16 2012 +0200
+++ b/src/Pure/System/build.scala	Wed Jul 18 17:17:38 2012 +0200
@@ -9,6 +9,8 @@
 
 import java.io.File
 
+import scala.collection.mutable
+
 
 object Build
 {
@@ -64,22 +66,37 @@
   }
 
 
-  /* session information */
-
-  val ROOT_NAME = "ROOT"
+  /** session information **/
 
   type Options = List[(String, Option[String])]
 
   case class Session_Info(
     dir: Path,
     name: String,
-    reset_name: Boolean,
     parent: 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,
+    description: String,
+    options: Options,
+    theories: List[(Options, List[String])],
+    files: List[String])
+
   private object Parser extends Parse.Parser
   {
     val SESSION = "session"
@@ -93,15 +110,14 @@
       Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
         SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
 
-    def session_info(dir: Path): Parser[Session_Info] =
+    val session_entry: Parser[Session_Entry] =
     {
       val session_name = atom("session name", _.is_name)
       val theory_name = atom("theory name", _.is_name)
 
       val option =
         name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
-      val options: Parser[Options] =
-        keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
+      val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
 
       val theories =
         keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
@@ -109,36 +125,65 @@
 
       ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
         (keyword("!") ^^^ true | success(false)) ~
-        (opt(keyword(IN) ~! string ^^ { case _ ~ x => Path.explode(x) })) ~
+        (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
         (keyword("=") ~> session_name <~ keyword("+")) ~
         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
         (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
-        rep(theories) ~
+        rep1(theories) ~
         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
-          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h =>
-              val dir1 = dir + c.getOrElse(Path.basic(a))
-              val thys = g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
-              Session_Info(dir1, a, b, d, e, f, thys, h) }
+          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) }
     }
 
-    def parse_entries(dir: Path, root: File): List[Session_Info] =
+    def parse_entries(root: File): List[Session_Entry] =
     {
       val toks = syntax.scan(Standard_System.read_file(root))
-      parse_all(rep(session_info(dir)), Token.reader(toks, root.toString)) match {
+      parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
       }
     }
   }
 
-  def find_sessions(): List[Session_Info] =
+
+  /* find session */
+
+  def find_sessions(more_dirs: List[Path] = Nil): List[Session_Info] =
   {
+    val infos = new mutable.ListBuffer[Session_Info]
+    infos += pure_info
+
     for {
-      dir <- Isabelle_System.components()
+      dir <- Isabelle_System.components() ++ more_dirs
       root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
       if root.isFile
-      entry <- Parser.parse_entries(dir, root)
-    } yield entry
+      entry <- Parser.parse_entries(root)
+    }
+    {
+      try {
+        val parent =
+          infos.find(_.name == entry.parent) getOrElse
+           error("Unknown parent session: " + quote(entry.parent))
+        val full_name =
+          if (entry.reset) entry.name
+          else parent.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)
+        infos += info
+      }
+      catch {
+        case ERROR(msg) =>
+          error(msg + "\nThe error(s) above occurred in session entry " +
+            quote(entry.name) + " (file " + quote(root.toString) + ")")
+      }
+    }
+    infos.toList
   }
 }