# HG changeset patch
# User wenzelm
# Date 1754861455 -7200
# Node ID 85887dcdef7fe377c69ec95ec1dda4a092b9e40d
# Parent  cbeab5584c62131f44ccaa14c30dfab6500f92a8
prefer Process_Theories over raw ML_Process;

diff -r cbeab5584c62 -r 85887dcdef7f src/Pure/Tools/profiling.scala
--- a/src/Pure/Tools/profiling.scala	Sun Aug 10 22:11:50 2025 +0200
+++ b/src/Pure/Tools/profiling.scala	Sun Aug 10 23:30:55 2025 +0200
@@ -71,24 +71,21 @@
 
     def make(
       store: Store,
-      session_background: Sessions.Background,
+      session_base: Sessions.Base,
+      dirs: List[Path] = Nil,
       parent: Option[Statistics] = None
     ): Statistics = {
-      val session_base = session_background.base
       val session_name = session_base.session_name
 
-      val session = {
-        val args = session_base.used_theories.map(p => p._1.theory)
-        val eval_args =
-          List("--eval", "use_thy " + ML_Syntax.print_string_bytes("~~/src/Tools/Profiling"))
+      val session =
         Isabelle_System.with_tmp_dir("profiling") { dir =>
-          File.write(dir + Path.explode("args.yxml"), YXML.string_of_body(encode_args(args)))
+          File.write(dir + Path.explode("args.yxml"),
+            YXML.string_of_body(encode_args(session_base.used_theories.map(p => p._1.theory))))
           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(ml_options, session_background, session_heaps, args = eval_args).result().check
+          Process_Theories.process_theories(ml_options, session_name,
+            dirs = dirs, files = List(Path.explode("~~/src/Tools/Profiling.thy"))).check
           decode_result(YXML.parse_body(Bytes.read(dir + Path.explode("result.yxml"))))
         }
-      }
 
       new Statistics(parent = parent, session = session_name,
         theories = session.theories,
@@ -247,12 +244,9 @@
       build_heap: Boolean = false,
       clean_build: Boolean = false
     ): Build.Results = {
-      val results =
-        Build.build(build_options, progress = progress,
-          selection = selection, build_heap = build_heap, clean_build = clean_build,
-          dirs = sessions_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs)
-
-      if (results.ok) results else error("Build failed")
+      Build.build(build_options, progress = progress,
+        selection = selection, build_heap = build_heap, clean_build = clean_build,
+        dirs = sessions_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs).check
     }
 
 
@@ -282,8 +276,8 @@
             parent_stats <- seen.get(parent_name)
           } yield parent_stats
         val stats =
-          Statistics.make(store,
-            build_results.deps.background(session_name),
+          Statistics.make(store, build_results.deps(session_name),
+            dirs = sessions_dirs,
             parent = parent)
         seen += (session_name -> stats)
         stats