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