src/Pure/PIDE/command.ML
changeset 53976 da610b507799
parent 53709 84522727f9d3
child 54519 5fed81762406
child 54637 db3d3d99c69d
--- a/src/Pure/PIDE/command.ML	Sun Sep 29 00:15:05 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Sun Sep 29 11:21:02 2013 +0200
@@ -318,7 +318,7 @@
 local
 
 fun run_print execution_id (Print {name, delay, pri, print_process, ...}) =
-  if Multithreading.enabled () then
+  if Multithreading.enabled () orelse pri <= 0 then
     let
       val group = Future.worker_subgroup ();
       fun fork () =