# HG changeset patch
# User wenzelm
# Date 1596833834 -7200
# Node ID d115d50a19c0239574783ce6f06f488539f48d6f
# Parent  84f716e72fa3023421ca5a6d29b5a04b4b0fadd2
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);

diff -r 84f716e72fa3 -r d115d50a19c0 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Fri Aug 07 22:28:04 2020 +0200
+++ b/src/Pure/ML/ml_process.scala	Fri Aug 07 22:57:14 2020 +0200
@@ -110,7 +110,9 @@
 
     // ISABELLE_TMP
     val isabelle_tmp = Isabelle_System.tmp_dir("process")
-    val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
+    val env_tmp =
+      Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp),
+        "POLYSTATSDIR" -> isabelle_tmp.getAbsolutePath)
 
     val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(","))
 
diff -r 84f716e72fa3 -r d115d50a19c0 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
       }
diff -r 84f716e72fa3 -r d115d50a19c0 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Aug 07 22:28:04 2020 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Aug 07 22:57:14 2020 +0200
@@ -209,7 +209,7 @@
   val dialogN: string val dialog: serial -> string -> T
   val jedit_actionN: string
   val functionN: string
-  val ML_statistics: {pid: int} -> Properties.T
+  val ML_statistics: {pid: int, stats_dir: string} -> Properties.T
   val commands_accepted: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
@@ -672,7 +672,8 @@
 
 val functionN = "function"
 
-fun ML_statistics {pid} = [(functionN, "ML_statistics"), ("pid", Value.print_int pid)];
+fun ML_statistics {pid, stats_dir} =
+  [(functionN, "ML_statistics"), ("pid", Value.print_int pid), ("stats_dir", stats_dir)];
 
 val commands_accepted = [(functionN, "commands_accepted")];
 
diff -r 84f716e72fa3 -r d115d50a19c0 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Aug 07 22:28:04 2020 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Aug 07 22:57:14 2020 +0200
@@ -578,9 +578,10 @@
 
   object ML_Statistics extends Function("ML_statistics")
   {
-    def unapply(props: Properties.T): Option[Long] =
+    def unapply(props: Properties.T): Option[(Long, String)] =
       props match {
-        case List(PROPERTY, ("pid", Value.Long(pid))) => Some(pid)
+        case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) =>
+          Some((pid, stats_dir))
         case _ => None
       }
   }
diff -r 84f716e72fa3 -r d115d50a19c0 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Aug 07 22:28:04 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Aug 07 22:57:14 2020 +0200
@@ -113,6 +113,10 @@
     Output.physical_stderr
       "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
 
+fun ml_statistics () =
+  Output.protocol_message
+    (Markup.ML_statistics {pid = ML_Pid.get (), stats_dir = getenv "POLYSTATSDIR"}) [];
+
 val _ = Session.protocol_handler "isabelle.ML_Statistics$Protocol_Handler";
 
 in
@@ -201,7 +205,7 @@
 
     fun protocol () =
      (Session.init_protocol_handlers ();
-      Output.protocol_message (Markup.ML_statistics {pid = ML_Pid.get ()}) [];
+      ml_statistics ();
       message Markup.initN [] [XML.Text (Session.welcome ())];
       protocol_loop ());