1 /* Title: Pure/System/build.scala
4 Build and manage Isabelle sessions.
12 import scala.collection.mutable
17 /* command line entry point */
21 def unapply(s: String): Option[Boolean] =
23 case "true" => Some(true)
24 case "false" => Some(false)
29 def main(args: Array[String])
31 def bad_args(): Nothing = error("Bad arguments: " + args.toString)
36 case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) :: rest =>
37 rest.indexWhere(_ == "\n") match {
40 val (options, rest1) = rest.splitAt(i)
41 val sessions = rest1.tail
42 build(all_sessions, build_images, list_only, options, sessions)
48 case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2
57 def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
58 options: List[String], sessions: List[String]): Int =
60 println("options = " + options.toString)
61 println("sessions = " + sessions.toString)
63 find_sessions() foreach println
69 /** session information **/
71 type Options = List[(String, Option[String])]
73 case class Session_Info(
79 theories: List[(Options, String)],
82 private val pure_info =
83 Session_Info(Path.current, "Pure", "", "", Nil, List((Nil, "Pure")), Nil)
88 val ROOT_NAME = "ROOT"
90 private case class Session_Entry(
97 theories: List[(Options, List[String])],
100 private object Parser extends Parse.Parser
102 val SESSION = "session"
104 val DESCRIPTION = "description"
105 val OPTIONS = "options"
106 val THEORIES = "theories"
110 Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
111 SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
113 val session_entry: Parser[Session_Entry] =
115 val session_name = atom("session name", _.is_name)
116 val theory_name = atom("theory name", _.is_name)
119 name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
120 val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
123 keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
124 { case _ ~ (x ~ y) => (x, y) }
126 ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
127 (keyword("!") ^^^ true | success(false)) ~
128 (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
129 (keyword("=") ~> session_name <~ keyword("+")) ~
130 (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
131 (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
133 (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
134 { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) }
137 def parse_entries(root: File): List[Session_Entry] =
139 val toks = syntax.scan(Standard_System.read_file(root))
140 parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
141 case Success(result, _) => result
142 case bad => error(bad.toString)
150 def find_sessions(more_dirs: List[Path] = Nil): List[Session_Info] =
152 val infos = new mutable.ListBuffer[Session_Info]
156 dir <- Isabelle_System.components() ++ more_dirs
157 root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
159 entry <- Parser.parse_entries(root)
164 infos.find(_.name == entry.parent) getOrElse
165 error("Unknown parent session: " + quote(entry.parent))
167 if (entry.reset) entry.name
168 else parent.name + "-" + entry.name
170 if (entry.name == "") error("Bad session name")
171 if (infos.exists(_.name == full_name))
172 error("Duplicate session name: " + quote(full_name))
176 case Some(p) => Path.explode(p)
177 case None => Path.basic(entry.name)
179 val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
181 Session_Info(dir + path, full_name, entry.parent, entry.description,
182 entry.options, thys, entry.files)
188 error(msg + "\nThe error(s) above occurred in session entry " +
189 quote(entry.name) + " (file " + quote(root.toString) + ")")