avoid global Output for "internal" ML process, notably from Isabelle/ML;
authorwenzelm
Sat, 08 Nov 2025 17:13:27 +0100
changeset 83528 eabf2d05787c
parent 83527 53d2488f1802
child 83529 55eb0e3838f9
avoid global Output for "internal" ML process, notably from Isabelle/ML;
src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sat Nov 08 15:33:18 2025 +0100
+++ b/src/Pure/ML/ml_process.scala	Sat Nov 08 17:13:27 2025 +0100
@@ -169,11 +169,16 @@
     val store = Store(options)
     val session_background = Sessions.background(options, logic, dirs = dirs).check_errors
     val session_heaps = store.session_heaps(session_background, logic = logic)
-    ML_Process(options, session_background, session_heaps,
-      args = eval_args, modes = modes, cwd = cwd, redirect = redirect)
-      .result(
+
+    val process =
+      ML_Process(options, session_background, session_heaps,
+        args = eval_args, modes = modes, cwd = cwd, redirect = redirect)
+    if (internal) process.result()
+    else {
+      process.result(
         progress_stdout = Output.writeln(_, stdout = true),
         progress_stderr = Output.writeln(_))
+    }
   }
 
   val isabelle_tool =