equal
deleted
inserted
replaced
97 } |
97 } |
98 |
98 |
99 private def consume(props: Properties.T): Unit = synchronized |
99 private def consume(props: Properties.T): Unit = synchronized |
100 { |
100 { |
101 if (session != null) { |
101 if (session != null) { |
102 val props1 = (session.xml_cache.props(props ::: Java_Statistics.jvm_statistics())) |
102 val props1 = (session.cache.props(props ::: Java_Statistics.jvm_statistics())) |
103 session.runtime_statistics.post(Session.Runtime_Statistics(props1)) |
103 session.runtime_statistics.post(Session.Runtime_Statistics(props1)) |
104 } |
104 } |
105 } |
105 } |
106 |
106 |
107 private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized |
107 private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized |