# HG changeset patch
# User wenzelm
# Date 1594807488 -7200
# Node ID 25d5ef16401a5d7d66664c5cdce3f8960686655a
# Parent  452073b64f28e2b73df1ef20f0ec90263cc2b55e
support for monitoring of external ML process;

diff -r 452073b64f28 -r 25d5ef16401a src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed Jul 15 11:56:43 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Wed Jul 15 12:04:48 2020 +0200
@@ -25,6 +25,31 @@
   def now(props: Properties.T): Double = Now.unapply(props).get
 
 
+  /* monitor process */
+
+  def monitor(pid: Long,
+    delay: Time = Time.seconds(0.5),
+    consume: Properties.T => Unit = Console.println)
+  {
+    def progress_stdout(line: String)
+    {
+      val props =
+        Library.space_explode(',', line).flatMap((entry: String) =>
+          Library.space_explode('=', entry) match {
+            case List(a, b) => Some((a, b))
+            case _ => None
+          })
+      if (props.nonEmpty) consume(props)
+    }
+
+    Bash.process("exec \"$POLYML_EXE\" -q --use " +
+      File.bash_path(Path.explode("~~/src/Pure/ML/ml_statistics.ML")) +
+      " --eval " + Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
+          ML_Syntax.print_double(delay.seconds)))
+      .result(progress_stdout = progress_stdout, strict = false).check
+  }
+
+
   /* memory fields (mega bytes) */
 
   def mem_print(x: Long): Option[String] =