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