prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf);
1.1 --- a/src/Pure/PIDE/command.ML Fri Aug 01 15:08:49 2014 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Fri Aug 01 22:52:53 2014 +0200
1.3 @@ -382,7 +382,7 @@
1.4 print_function "Execution.print"
1.5 (fn {args, exec_id, ...} =>
1.6 if null args then
1.7 - SOME {delay = NONE, pri = 1, persistent = false, strict = true,
1.8 + SOME {delay = NONE, pri = 1, persistent = false, strict = false,
1.9 print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
1.10 else NONE);
1.11