1 /* Title: Pure/System/build.scala
4 Build and manage Isabelle sessions.
15 /* command line entry point */
19 def unapply(s: String): Option[Boolean] =
21 case "true" => Some(true)
22 case "false" => Some(false)
27 def main(args: Array[String])
29 def bad_args(): Nothing = error("Bad arguments: " + args.toString)
34 case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) :: rest =>
35 rest.indexWhere(_ == "\n") match {
38 val (options, rest1) = rest.splitAt(i)
39 val sessions = rest1.tail
40 build(all_sessions, build_images, list_only, options, sessions)
46 case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2
55 def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
56 options: List[String], sessions: List[String]): Int =
58 println("options = " + options.toString)
59 println("sessions = " + sessions.toString)
61 find_sessions() foreach println
67 /* session information */
69 val ROOT_NAME = "ROOT"
71 type Options = List[(String, Option[String])]
73 case class Session_Info(
80 theories: List[(Options, String)],
83 private object Parser extends Parse.Parser
85 val SESSION = "session"
87 val DESCRIPTION = "description"
88 val OPTIONS = "options"
89 val THEORIES = "theories"
93 Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
94 SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
96 def session_info(dir: Path): Parser[Session_Info] =
98 val session_name = atom("session name", _.is_name)
99 val theory_name = atom("theory name", _.is_name)
102 name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
103 val options: Parser[Options] =
104 keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
107 keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
108 { case _ ~ (x ~ y) => (x, y) }
110 ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
111 (keyword("!") ^^^ true | success(false)) ~
112 (opt(keyword(IN) ~! string ^^ { case _ ~ x => Path.explode(x) })) ~
113 (keyword("=") ~> session_name <~ keyword("+")) ~
114 (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
115 (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
117 (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
118 { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h =>
119 val dir1 = dir + c.getOrElse(Path.basic(a))
120 val thys = g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
121 Session_Info(dir1, a, b, d, e, f, thys, h) }
124 def parse_entries(dir: Path, root: File): List[Session_Info] =
126 val toks = syntax.scan(Standard_System.read_file(root))
127 parse_all(rep(session_info(dir)), Token.reader(toks, root.toString)) match {
128 case Success(result, _) => result
129 case bad => error(bad.toString)
134 def find_sessions(): List[Session_Info] =
137 dir <- Isabelle_System.components()
138 root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
140 entry <- Parser.parse_entries(dir, root)