13 import scala.annotation.tailrec |
13 import scala.annotation.tailrec |
14 |
14 |
15 |
15 |
16 object Build |
16 object Build |
17 { |
17 { |
18 /* command line entry point */ |
18 /** session information **/ |
|
19 |
|
20 type Options = List[(String, Option[String])] |
|
21 |
|
22 case class Session_Info( |
|
23 dir: Path, |
|
24 name: String, |
|
25 parent: String, |
|
26 description: String, |
|
27 options: Options, |
|
28 theories: List[(Options, String)], |
|
29 files: List[String]) |
|
30 |
|
31 private val pure_info = |
|
32 Session_Info(Path.current, "Pure", "", "", Nil, List((Nil, "Pure")), Nil) |
|
33 |
|
34 |
|
35 /* parsing */ |
|
36 |
|
37 val ROOT_NAME = "ROOT" |
|
38 |
|
39 private case class Session_Entry( |
|
40 name: String, |
|
41 reset: Boolean, |
|
42 path: Option[String], |
|
43 parent: String, |
|
44 description: String, |
|
45 options: Options, |
|
46 theories: List[(Options, List[String])], |
|
47 files: List[String]) |
|
48 |
|
49 private object Parser extends Parse.Parser |
|
50 { |
|
51 val SESSION = "session" |
|
52 val IN = "in" |
|
53 val DESCRIPTION = "description" |
|
54 val OPTIONS = "options" |
|
55 val THEORIES = "theories" |
|
56 val FILES = "files" |
|
57 |
|
58 val syntax = |
|
59 Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" + |
|
60 SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES |
|
61 |
|
62 val session_entry: Parser[Session_Entry] = |
|
63 { |
|
64 val session_name = atom("session name", _.is_name) |
|
65 val theory_name = atom("theory name", _.is_name) |
|
66 |
|
67 val option = |
|
68 name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) } |
|
69 val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]") |
|
70 |
|
71 val theories = |
|
72 keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^ |
|
73 { case _ ~ (x ~ y) => (x, y) } |
|
74 |
|
75 ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~ |
|
76 (keyword("!") ^^^ true | success(false)) ~ |
|
77 (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~ |
|
78 (keyword("=") ~> session_name <~ keyword("+")) ~ |
|
79 (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~ |
|
80 (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~ |
|
81 rep1(theories) ~ |
|
82 (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^ |
|
83 { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) } |
|
84 } |
|
85 |
|
86 def parse_entries(root: File): List[Session_Entry] = |
|
87 { |
|
88 val toks = syntax.scan(Standard_System.read_file(root)) |
|
89 parse_all(rep(session_entry), Token.reader(toks, root.toString)) match { |
|
90 case Success(result, _) => result |
|
91 case bad => error(bad.toString) |
|
92 } |
|
93 } |
|
94 } |
|
95 |
|
96 |
|
97 /* find sessions */ |
|
98 |
|
99 def find_sessions(more_dirs: List[Path]): List[Session_Info] = |
|
100 { |
|
101 val infos = new mutable.ListBuffer[Session_Info] |
|
102 infos += pure_info |
|
103 |
|
104 for { |
|
105 (dir, strict) <- Isabelle_System.components().map((_, false)) ++ more_dirs.map((_, true)) |
|
106 root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME)) |
|
107 _ = (strict && !root.isFile && error("Bad session root file: " + quote(root.toString))) |
|
108 if root.isFile |
|
109 entry <- Parser.parse_entries(root) |
|
110 } |
|
111 { |
|
112 try { |
|
113 val parent = |
|
114 infos.find(_.name == entry.parent) getOrElse |
|
115 error("Unknown parent session: " + quote(entry.parent)) |
|
116 val full_name = |
|
117 if (entry.reset) entry.name |
|
118 else parent.name + "-" + entry.name |
|
119 |
|
120 if (entry.name == "") error("Bad session name") |
|
121 if (infos.exists(_.name == full_name)) |
|
122 error("Duplicate session name: " + quote(full_name)) |
|
123 |
|
124 val path = |
|
125 entry.path match { |
|
126 case Some(p) => Path.explode(p) |
|
127 case None => Path.basic(entry.name) |
|
128 } |
|
129 val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten |
|
130 val info = |
|
131 Session_Info(dir + path, full_name, entry.parent, entry.description, |
|
132 entry.options, thys, entry.files) |
|
133 |
|
134 infos += info |
|
135 } |
|
136 catch { |
|
137 case ERROR(msg) => |
|
138 error(msg + "\nThe error(s) above occurred in session entry " + |
|
139 quote(entry.name) + " (file " + quote(root.toString) + ")") |
|
140 } |
|
141 } |
|
142 infos.toList |
|
143 } |
|
144 |
|
145 |
|
146 |
|
147 /** build **/ |
|
148 |
|
149 def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean, |
|
150 more_dirs: List[Path], options: List[String], sessions: List[String]): Int = |
|
151 { |
|
152 println("more_dirs = " + more_dirs.toString) |
|
153 println("options = " + options.toString) |
|
154 println("sessions = " + sessions.toString) |
|
155 |
|
156 find_sessions(more_dirs) foreach println |
|
157 |
|
158 0 |
|
159 } |
|
160 |
|
161 |
|
162 |
|
163 /** command line entry point **/ |
19 |
164 |
20 private object Bool |
165 private object Bool |
21 { |
166 { |
22 def unapply(s: String): Option[Boolean] = |
167 def unapply(s: String): Option[Boolean] = |
23 s match { |
168 s match { |
54 catch { |
199 catch { |
55 case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2 |
200 case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2 |
56 } |
201 } |
57 sys.exit(rc) |
202 sys.exit(rc) |
58 } |
203 } |
59 |
|
60 |
|
61 /* build */ |
|
62 |
|
63 def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean, |
|
64 more_dirs: List[Path], options: List[String], sessions: List[String]): Int = |
|
65 { |
|
66 println("more_dirs = " + more_dirs.toString) |
|
67 println("options = " + options.toString) |
|
68 println("sessions = " + sessions.toString) |
|
69 |
|
70 find_sessions(more_dirs) foreach println |
|
71 |
|
72 0 |
|
73 } |
|
74 |
|
75 |
|
76 /** session information **/ |
|
77 |
|
78 type Options = List[(String, Option[String])] |
|
79 |
|
80 case class Session_Info( |
|
81 dir: Path, |
|
82 name: String, |
|
83 parent: String, |
|
84 description: String, |
|
85 options: Options, |
|
86 theories: List[(Options, String)], |
|
87 files: List[String]) |
|
88 |
|
89 private val pure_info = |
|
90 Session_Info(Path.current, "Pure", "", "", Nil, List((Nil, "Pure")), Nil) |
|
91 |
|
92 |
|
93 /* parsing */ |
|
94 |
|
95 val ROOT_NAME = "ROOT" |
|
96 |
|
97 private case class Session_Entry( |
|
98 name: String, |
|
99 reset: Boolean, |
|
100 path: Option[String], |
|
101 parent: String, |
|
102 description: String, |
|
103 options: Options, |
|
104 theories: List[(Options, List[String])], |
|
105 files: List[String]) |
|
106 |
|
107 private object Parser extends Parse.Parser |
|
108 { |
|
109 val SESSION = "session" |
|
110 val IN = "in" |
|
111 val DESCRIPTION = "description" |
|
112 val OPTIONS = "options" |
|
113 val THEORIES = "theories" |
|
114 val FILES = "files" |
|
115 |
|
116 val syntax = |
|
117 Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" + |
|
118 SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES |
|
119 |
|
120 val session_entry: Parser[Session_Entry] = |
|
121 { |
|
122 val session_name = atom("session name", _.is_name) |
|
123 val theory_name = atom("theory name", _.is_name) |
|
124 |
|
125 val option = |
|
126 name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) } |
|
127 val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]") |
|
128 |
|
129 val theories = |
|
130 keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^ |
|
131 { case _ ~ (x ~ y) => (x, y) } |
|
132 |
|
133 ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~ |
|
134 (keyword("!") ^^^ true | success(false)) ~ |
|
135 (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~ |
|
136 (keyword("=") ~> session_name <~ keyword("+")) ~ |
|
137 (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~ |
|
138 (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~ |
|
139 rep1(theories) ~ |
|
140 (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^ |
|
141 { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) } |
|
142 } |
|
143 |
|
144 def parse_entries(root: File): List[Session_Entry] = |
|
145 { |
|
146 val toks = syntax.scan(Standard_System.read_file(root)) |
|
147 parse_all(rep(session_entry), Token.reader(toks, root.toString)) match { |
|
148 case Success(result, _) => result |
|
149 case bad => error(bad.toString) |
|
150 } |
|
151 } |
|
152 } |
|
153 |
|
154 |
|
155 /* find session */ |
|
156 |
|
157 def find_sessions(more_dirs: List[Path]): List[Session_Info] = |
|
158 { |
|
159 val infos = new mutable.ListBuffer[Session_Info] |
|
160 infos += pure_info |
|
161 |
|
162 for { |
|
163 (dir, strict) <- Isabelle_System.components().map((_, false)) ++ more_dirs.map((_, true)) |
|
164 root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME)) |
|
165 _ = (strict && !root.isFile && error("Bad session root file: " + quote(root.toString))) |
|
166 if root.isFile |
|
167 entry <- Parser.parse_entries(root) |
|
168 } |
|
169 { |
|
170 try { |
|
171 val parent = |
|
172 infos.find(_.name == entry.parent) getOrElse |
|
173 error("Unknown parent session: " + quote(entry.parent)) |
|
174 val full_name = |
|
175 if (entry.reset) entry.name |
|
176 else parent.name + "-" + entry.name |
|
177 |
|
178 if (entry.name == "") error("Bad session name") |
|
179 if (infos.exists(_.name == full_name)) |
|
180 error("Duplicate session name: " + quote(full_name)) |
|
181 |
|
182 val path = |
|
183 entry.path match { |
|
184 case Some(p) => Path.explode(p) |
|
185 case None => Path.basic(entry.name) |
|
186 } |
|
187 val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten |
|
188 val info = |
|
189 Session_Info(dir + path, full_name, entry.parent, entry.description, |
|
190 entry.options, thys, entry.files) |
|
191 |
|
192 infos += info |
|
193 } |
|
194 catch { |
|
195 case ERROR(msg) => |
|
196 error(msg + "\nThe error(s) above occurred in session entry " + |
|
197 quote(entry.name) + " (file " + quote(root.toString) + ")") |
|
198 } |
|
199 } |
|
200 infos.toList |
|
201 } |
|
202 } |
204 } |
203 |
205 |