--- a/src/Pure/ML/ml_statistics.scala Sun Jun 15 22:14:38 2025 +0200
+++ b/src/Pure/ML/ml_statistics.scala Sun Jun 15 22:46:45 2025 +0200
@@ -47,7 +47,7 @@
/* monitor process */
- def monitor(pid: Long,
+ def monitor(options: Options, pid: Long,
stats_dir: String = "",
delay: Time = Time.seconds(0.5),
consume: Properties.T => Unit = Console.println
@@ -59,7 +59,10 @@
val env_prefix = if_proper(stats_dir, Bash.exports("POLYSTATSDIR=" + stats_dir))
- Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
+ val polyml_exe = ML_Settings.system(options).polyml_exe
+
+ Bash.process(env_prefix + File.bash_path(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.ISABELLE_HOME)
@@ -94,7 +97,7 @@
case Markup.ML_Statistics(pid, stats_dir) =>
monitoring =
Future.thread("ML_statistics") {
- monitor(pid, stats_dir = stats_dir, consume = consume)
+ monitor(session.session_options, pid, stats_dir = stats_dir, consume = consume)
}
true
case _ => false