prefer system options, which are easier to change on the spot;
authorwenzelm
Sun, 10 Aug 2025 21:44:42 +0200
changeset 82979 98faa43a2505
parent 82978 85c982ddc82d
child 82980 839d86abfe86
prefer system options, which are easier to change on the spot;
etc/options
src/Pure/Tools/profiling.scala
src/Tools/Profiling.thy
--- a/etc/options	Sun Aug 10 21:09:45 2025 +0200
+++ b/etc/options	Sun Aug 10 21:44:42 2025 +0200
@@ -161,6 +161,9 @@
 option profiling : string = "" (standard "time") for build
   -- "ML profiling (possible values: time, time_thread, allocations)"
 
+option profiling_dir : string = "" for content
+  -- "output directory for \"isabelle profiling\" tool"
+
 option system_log : string = "" (standard "-") for build
   -- "output for system messages (log file or \"-\" for console progress)"
 
--- a/src/Pure/Tools/profiling.scala	Sun Aug 10 21:09:45 2025 +0200
+++ b/src/Pure/Tools/profiling.scala	Sun Aug 10 21:44:42 2025 +0200
@@ -82,11 +82,10 @@
         val eval_args =
           List("--eval", "use_thy " + ML_Syntax.print_string_bytes("~~/src/Tools/Profiling"))
         Isabelle_System.with_tmp_dir("profiling") { dir =>
-          val putenv = List("ISABELLE_PROFILING" -> dir.implode)
           File.write(dir + Path.explode("args.yxml"), YXML.string_of_body(encode_args(args)))
+          val ml_options = store.options + Options.Spec("profiling_dir", Some(dir.implode))
           val session_heaps = store.session_heaps(session_background, logic = session_name)
-          ML_Process(store.options, session_background, session_heaps, args = eval_args,
-            env = Isabelle_System.Settings.env(putenv)).result().check
+          ML_Process(ml_options, session_background, session_heaps, args = eval_args).result().check
           decode_result(YXML.parse_body(Bytes.read(dir + Path.explode("result.yxml"))))
         }
       }
--- a/src/Tools/Profiling.thy	Sun Aug 10 21:09:45 2025 +0200
+++ b/src/Tools/Profiling.thy	Sun Aug 10 21:44:42 2025 +0200
@@ -183,7 +183,7 @@
 in
 
 fun main () =
-  (case getenv "ISABELLE_PROFILING" of
+  (case Options.default_string \<^system_option>\<open>profiling_dir\<close> of
     "" => ()
   | dir_name =>
       let