equal
deleted
inserted
replaced
73 if (session != null && session.session_options.bool("ML_statistics")) { |
73 if (session != null && session.session_options.bool("ML_statistics")) { |
74 session.runtime_statistics.post(Session.Runtime_Statistics(props)) |
74 session.runtime_statistics.post(Session.Runtime_Statistics(props)) |
75 } |
75 } |
76 } |
76 } |
77 |
77 |
78 private def ml_pid(msg: Prover.Protocol_Output): Boolean = synchronized |
78 private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized |
79 { |
79 { |
80 msg.properties match { |
80 msg.properties match { |
81 case Markup.ML_Pid(pid) => |
81 case Markup.ML_Statistics(pid) => |
82 monitoring = Future.thread("ML_statistics") { monitor(pid, consume = consume) } |
82 monitoring = Future.thread("ML_statistics") { monitor(pid, consume = consume) } |
83 true |
83 true |
84 case _ => false |
84 case _ => false |
85 } |
85 } |
86 } |
86 } |
87 |
87 |
88 val functions = List(Markup.ML_Pid.name -> ml_pid) |
88 val functions = List(Markup.ML_Statistics.name -> ml_statistics) |
89 } |
89 } |
90 |
90 |
91 |
91 |
92 /* memory fields (mega bytes) */ |
92 /* memory fields (mega bytes) */ |
93 |
93 |