src/Pure/ML/ml_statistics.scala

     Bash.process("exec \"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
         Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
           ML_Syntax.print_double(delay.seconds)),
         cwd = Path.explode("~~").file)
       .result(progress_stdout = progress_stdout, strict = false).check
+  }
+
+
+  /* protocol handler */
+
+  class Protocol_Handler extends Session.Protocol_Handler
+  {
+    private var session: Session = null
+    private var monitoring: Future[Unit] = Future.value(())
+
+    override def init(init_session: Session): Unit = synchronized
+    {
+      session = init_session
+    }
+
+    override def exit(): Unit = synchronized
+    {
+      session = null
+      monitoring.cancel
+    }
+
+    private def consume(props: Properties.T): Unit = synchronized
+    {
+      if (session != null && session.session_options.bool("ML_statistics")) {
+        session.runtime_statistics.post(Session.Runtime_Statistics(props))
+      }
+    }
+
+    private def ml_pid(msg: Prover.Protocol_Output): Boolean = synchronized
+    {
+      msg.properties match {
+        case Markup.ML_Pid(pid) =>
+          monitoring = Future.thread("ML_statistics") { monitor(pid, consume = consume) }
+          true
+        case _ => false
+      }
+    }
+
+    val functions = List(Markup.ML_Pid.name -> ml_pid)
   }
 
 
   /* memory fields (mega bytes) */