equal
deleted
inserted
replaced
355 sessions_structure: Structure, |
355 sessions_structure: Structure, |
356 errors: List[String], |
356 errors: List[String], |
357 base: Base, |
357 base: Base, |
358 infos: List[Info]) |
358 infos: List[Info]) |
359 { |
359 { |
360 def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors)) |
360 def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors)) |
361 } |
361 } |
362 |
362 |
363 def base_info(options: Options, |
363 def base_info(options: Options, |
364 session: String, |
364 session: String, |
365 progress: Progress = new Progress, |
365 progress: Progress = new Progress, |