src/Pure/ML/ml_statistics.scala

--- a/src/Pure/ML/ml_statistics.scala	Fri Aug 07 22:28:04 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Fri Aug 07 22:57:14 2020 +0200
@@ -28,6 +28,7 @@
   /* monitor process */
 
   def monitor(pid: Long,
+    stats_dir: String = "",
     delay: Time = Time.seconds(0.5),
     consume: Properties.T => Unit = Console.println)
   {
@@ -42,7 +43,10 @@
       if (props.nonEmpty) consume(props)
     }
 
-    Bash.process("exec \"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
+    val env_prefix =
+      if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n"
+
+    Bash.process(env_prefix + "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)
@@ -79,8 +83,11 @@
     private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized
     {
       msg.properties match {
-        case Markup.ML_Statistics(pid) =>
-          monitoring = Future.thread("ML_statistics") { monitor(pid, consume = consume) }
+        case Markup.ML_Statistics(pid, stats_dir) =>
+          monitoring =
+            Future.thread("ML_statistics") {
+              monitor(pid, stats_dir = stats_dir, consume = consume)
+            }
           true
         case _ => false
       }