prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf);
authorwenzelm
Fri, 01 Aug 2014 22:52:53 +0200
changeset 57839 d5b0fa6f1f7a
parent 57838 c21f2c52f54b
child 57840 074cb68b40a8
prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf);
src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Aug 01 15:08:49 2014 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Aug 01 22:52:53 2014 +0200
@@ -382,7 +382,7 @@
   print_function "Execution.print"
     (fn {args, exec_id, ...} =>
       if null args then
-        SOME {delay = NONE, pri = 1, persistent = false, strict = true,
+        SOME {delay = NONE, pri = 1, persistent = false, strict = false,
           print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
       else NONE);