src/Pure/PIDE/document.ML

--- a/src/Pure/PIDE/document.ML	Wed Feb 20 21:20:30 2019 +0100
+++ b/src/Pure/PIDE/document.ML	Wed Feb 20 21:54:52 2019 +0100
@@ -498,7 +498,7 @@
       val delay = seconds (Options.default_real "editor_execution_delay");
 
       val _ = Future.cancel delay_request;
-      val delay_request' = Event_Timer.future (Time.now () + delay);
+      val delay_request' = Event_Timer.future {physical = true} (Time.now () + delay);
       val delay = Future.task_of delay_request';
 
       val parallel_prints' = parallel_prints