385 start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList, |
385 start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList, |
386 log_file.get_all_settings) |
386 log_file.get_all_settings) |
387 } |
387 } |
388 |
388 |
389 log_file.lines match { |
389 log_file.lines match { |
390 case line :: _ if Meta_Info_Marker.test_yxml(line) => |
390 case line :: _ if Protocol.Meta_Info_Marker.test_yxml(line) => |
391 Meta_Info(log_file.find_props(Meta_Info_Marker).get, log_file.get_all_settings) |
391 Meta_Info(log_file.find_props(Protocol.Meta_Info_Marker).get, log_file.get_all_settings) |
392 |
392 |
393 case Identify.Start(log_file.Strict_Date(start)) :: _ => |
393 case Identify.Start(log_file.Strict_Date(start)) :: _ => |
394 parse(Identify.engine(log_file), "", start, Identify.No_End, |
394 parse(Identify.engine(log_file), "", start, Identify.No_End, |
395 Identify.Isabelle_Version, Identify.AFP_Version) |
395 Identify.Isabelle_Version, Identify.AFP_Version) |
396 |
396 |
429 |
429 |
430 |
430 |
431 |
431 |
432 /** build info: toplevel output of isabelle build or Admin/build_history **/ |
432 /** build info: toplevel output of isabelle build or Admin/build_history **/ |
433 |
433 |
434 val Meta_Info_Marker = Protocol_Message.Marker("meta_info") |
|
435 val Timing_Marker = Protocol_Message.Marker("Timing") |
|
436 val Command_Timing_Marker = Protocol_Message.Marker("command_timing") |
|
437 val Theory_Timing_Marker = Protocol_Message.Marker("theory_timing") |
|
438 val ML_Statistics_Marker = Protocol_Message.Marker("ML_statistics") |
|
439 val Task_Statistics_Marker = Protocol_Message.Marker("task_statistics") |
|
440 val Error_Message_Marker = Protocol_Message.Marker("error_message") |
|
441 val SESSION_NAME = "session_name" |
434 val SESSION_NAME = "session_name" |
442 |
435 |
443 object Session_Status extends Enumeration |
436 object Session_Status extends Enumeration |
444 { |
437 { |
445 val existing, finished, failed, cancelled = Value |
438 val existing, finished, failed, cancelled = Value |
501 val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""") |
494 val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""") |
502 |
495 |
503 object Theory_Timing |
496 object Theory_Timing |
504 { |
497 { |
505 def unapply(line: String): Option[(String, (String, Timing))] = |
498 def unapply(line: String): Option[(String, (String, Timing))] = |
506 Theory_Timing_Marker.unapply(line.replace('~', '-')).map(log_file.parse_props) match { |
499 Protocol.Theory_Timing_Marker.unapply(line.replace('~', '-')).map(log_file.parse_props) |
|
500 match { |
507 case Some((SESSION_NAME, name) :: props) => |
501 case Some((SESSION_NAME, name) :: props) => |
508 (props, props) match { |
502 (props, props) match { |
509 case (Markup.Name(thy), Markup.Timing_Properties(t)) => Some((name, thy -> t)) |
503 case (Markup.Name(thy), Markup.Timing_Properties(t)) => Some((name, thy -> t)) |
510 case _ => None |
504 case _ => None |
511 } |
505 } |
570 sources += (name -> s) |
564 sources += (name -> s) |
571 |
565 |
572 case Heap(name, Value.Long(size)) => |
566 case Heap(name, Value.Long(size)) => |
573 heap_sizes += (name -> size) |
567 heap_sizes += (name -> size) |
574 |
568 |
575 case _ if Theory_Timing_Marker.test_yxml(line) => |
569 case _ if Protocol.Theory_Timing_Marker.test_yxml(line) => |
576 line match { |
570 line match { |
577 case Theory_Timing(name, theory_timing) => |
571 case Theory_Timing(name, theory_timing) => |
578 theory_timings += (name -> (theory_timings.getOrElse(name, Map.empty) + theory_timing)) |
572 theory_timings += (name -> (theory_timings.getOrElse(name, Map.empty) + theory_timing)) |
579 case _ => log_file.err("malformed theory_timing " + quote(line)) |
573 case _ => log_file.err("malformed theory_timing " + quote(line)) |
580 } |
574 } |
581 |
575 |
582 case _ if parse_ml_statistics && ML_Statistics_Marker.test_yxml(line) => |
576 case _ if parse_ml_statistics && Protocol.ML_Statistics_Marker.test_yxml(line) => |
583 ML_Statistics_Marker.unapply(line).map(log_file.parse_props) match { |
577 Protocol.ML_Statistics_Marker.unapply(line).map(log_file.parse_props) match { |
584 case Some((SESSION_NAME, name) :: props) => |
578 case Some((SESSION_NAME, name) :: props) => |
585 ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil))) |
579 ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil))) |
586 case _ => log_file.err("malformed ML_statistics " + quote(line)) |
580 case _ => log_file.err("malformed ML_statistics " + quote(line)) |
587 } |
581 } |
588 |
582 |
589 case _ if Error_Message_Marker.test_yxml(line) => |
583 case _ if Protocol.Error_Message_Marker.test_yxml(line) => |
590 Error_Message_Marker.unapply(line).map(log_file.parse_props) match { |
584 Protocol.Error_Message_Marker.unapply(line).map(log_file.parse_props) match { |
591 case Some(List((SESSION_NAME, name), (Markup.CONTENT, msg))) => |
585 case Some(List((SESSION_NAME, name), (Markup.CONTENT, msg))) => |
592 errors += (name -> (msg :: errors.getOrElse(name, Nil))) |
586 errors += (name -> (msg :: errors.getOrElse(name, Nil))) |
593 case _ => log_file.err("malformed error message " + quote(line)) |
587 case _ => log_file.err("malformed error message " + quote(line)) |
594 } |
588 } |
595 |
589 |
647 theory_timings: Boolean, |
641 theory_timings: Boolean, |
648 ml_statistics: Boolean, |
642 ml_statistics: Boolean, |
649 task_statistics: Boolean): Session_Info = |
643 task_statistics: Boolean): Session_Info = |
650 { |
644 { |
651 Session_Info( |
645 Session_Info( |
652 session_timing = log_file.find_props(Timing_Marker) getOrElse Nil, |
646 session_timing = log_file.find_props(Protocol.Timing_Marker) getOrElse Nil, |
653 command_timings = if (command_timings) log_file.filter_props(Command_Timing_Marker) else Nil, |
647 command_timings = |
654 theory_timings = if (theory_timings) log_file.filter_props(Theory_Timing_Marker) else Nil, |
648 if (command_timings) log_file.filter_props(Protocol.Command_Timing_Marker) else Nil, |
655 ml_statistics = if (ml_statistics) log_file.filter_props(ML_Statistics_Marker) else Nil, |
649 theory_timings = |
656 task_statistics = if (task_statistics) log_file.filter_props(Task_Statistics_Marker) else Nil, |
650 if (theory_timings) log_file.filter_props(Protocol.Theory_Timing_Marker) else Nil, |
657 errors = log_file.filter(Error_Message_Marker)) |
651 ml_statistics = |
|
652 if (ml_statistics) log_file.filter_props(Protocol.ML_Statistics_Marker) else Nil, |
|
653 task_statistics = |
|
654 if (task_statistics) log_file.filter_props(Protocol.Task_Statistics_Marker) else Nil, |
|
655 errors = log_file.filter(Protocol.Error_Message_Marker)) |
658 } |
656 } |
659 |
657 |
660 def compress_errors(errors: List[String], cache: XZ.Cache = XZ.cache()): Option[Bytes] = |
658 def compress_errors(errors: List[String], cache: XZ.Cache = XZ.cache()): Option[Bytes] = |
661 if (errors.isEmpty) None |
659 if (errors.isEmpty) None |
662 else { |
660 else { |