equal
deleted
inserted
replaced
245 |
245 |
246 /** meta info **/ |
246 /** meta info **/ |
247 |
247 |
248 object Field |
248 object Field |
249 { |
249 { |
|
250 val build_group_id = "build_group_id" |
|
251 val build_id = "build_id" |
250 val build_engine = "build_engine" |
252 val build_engine = "build_engine" |
251 val build_host = "build_host" |
253 val build_host = "build_host" |
252 val build_start = "build_start" |
254 val build_start = "build_start" |
253 val build_end = "build_end" |
255 val build_end = "build_end" |
254 val isabelle_version = "isabelle_version" |
256 val isabelle_version = "isabelle_version" |
301 private def parse_meta_info(log_file: Log_File): Meta_Info = |
303 private def parse_meta_info(log_file: Log_File): Meta_Info = |
302 { |
304 { |
303 def parse(engine: String, host: String, start: Date, |
305 def parse(engine: String, host: String, start: Date, |
304 End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info = |
306 End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info = |
305 { |
307 { |
|
308 val build_id = |
|
309 { |
|
310 val prefix = if (host != "") host else if (engine != "") engine else "" |
|
311 (if (prefix == "") "build" else prefix) + ":" + start.time.ms |
|
312 } |
306 val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine) |
313 val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine) |
307 val build_host = if (host == "") Nil else List(Field.build_host -> host) |
314 val build_host = if (host == "") Nil else List(Field.build_host -> host) |
308 |
315 |
309 val start_date = List(Field.build_start -> start.toString) |
316 val start_date = List(Field.build_start -> start.toString) |
310 val end_date = |
317 val end_date = |
317 val isabelle_version = |
324 val isabelle_version = |
318 log_file.find_match(Isabelle_Version).map(Field.isabelle_version -> _) |
325 log_file.find_match(Isabelle_Version).map(Field.isabelle_version -> _) |
319 val afp_version = |
326 val afp_version = |
320 log_file.find_match(AFP_Version).map(Field.afp_version -> _) |
327 log_file.find_match(AFP_Version).map(Field.afp_version -> _) |
321 |
328 |
322 Meta_Info(build_engine ::: build_host ::: |
329 Meta_Info((Field.build_id -> build_id) :: build_engine ::: build_host ::: |
323 start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList, |
330 start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList, |
324 log_file.get_settings(Settings.all_settings)) |
331 log_file.get_settings(Settings.all_settings)) |
325 } |
332 } |
326 |
333 |
327 log_file.lines match { |
334 log_file.lines match { |