553 default_name: String, |
553 default_name: String, |
554 command_timings: Boolean, |
554 command_timings: Boolean, |
555 ml_statistics: Boolean, |
555 ml_statistics: Boolean, |
556 task_statistics: Boolean): Session_Info = |
556 task_statistics: Boolean): Session_Info = |
557 { |
557 { |
558 val xml_cache = new XML.Cache() |
558 Session_Info( |
559 |
559 session_name = |
560 val session_name = |
560 log_file.find_line("\fSession.name = ") match { |
561 log_file.find_line("\fSession.name = ") match { |
561 case None => default_name |
562 case None => default_name |
562 case Some(name) if default_name == "" || default_name == name => name |
563 case Some(name) if default_name == "" || default_name == name => name |
563 case Some(name) => log_file.err("log from different session " + quote(name)) |
564 case Some(name) => log_file.err("log from different session " + quote(name)) |
564 }, |
565 } |
565 session_timing = log_file.find_props("\fTiming = ") getOrElse Nil, |
566 val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil |
566 command_timings = if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil, |
567 val command_timings_ = |
567 ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil, |
568 if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil |
568 task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil) |
569 val ml_statistics_ = |
|
570 if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil |
|
571 val task_statistics_ = |
|
572 if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil |
|
573 |
|
574 Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_) |
|
575 } |
569 } |
576 } |
570 } |