physical vs. logical events, the latter takes GC time into account;
Timeout.apply is based on logical ML time;

--- a/src/Pure/Concurrent/event_timer.ML	Wed Feb 20 21:20:30 2019 +0100
+++ b/src/Pure/Concurrent/event_timer.ML	Wed Feb 20 21:54:52 2019 +0100
@@ -11,9 +11,9 @@
 sig
   type request
   val eq_request: request * request -> bool
-  val request: Time.time -> (unit -> unit) -> request
+  val request: {physical: bool} -> Time.time -> (unit -> unit) -> request
   val cancel: request -> bool
-  val future: Time.time -> unit future
+  val future: {physical: bool} -> Time.time -> unit future
   val shutdown: unit -> unit
 end;
 
@@ -23,18 +23,20 @@
 (* type request *)
 
 datatype request =
-  Request of {id: int, time: Time.time, event: unit -> unit};
+  Request of {id: int, gc_start: Time.time option, time: Time.time, event: unit -> unit};
 
 val new_id = Counter.make ();
 
-fun new_request time event =
+fun new_request physical time event =
   Request {
     id = new_id (),
+    gc_start = if physical then NONE else SOME (ML_Heap.gc_now ()),
     time = time,
     event = event};
 
 fun eq_request (Request {id = id1, ...}, Request {id = id2, ...}) = id1 = id2;
 
+fun request_gc_start (Request {gc_start, ...}) = gc_start;
 fun request_time (Request {time, ...}) = time;
 fun request_event (Request {event, ...}) = event;
 
@@ -62,7 +64,7 @@
 fun next_time (requests: requests) =
   Option.map #1 (Requests.min requests);
 
-fun next_event now (requests: requests) =
+fun next_event (now, gc_now) (requests: requests) =
   (case Requests.min requests of
     NONE => NONE
   | SOME (req_time, reqs) =>
@@ -74,7 +76,15 @@
             if null reqs'
             then Requests.delete req_time requests
             else Requests.update (req_time, reqs') requests;
-        in SOME (request_event req, requests') end);
+          val req_time' =
+            (case request_gc_start req of
+              NONE => req_time
+            | SOME gc_start => request_time req + (gc_now - gc_start));
+        in
+          if now < req_time'
+          then (fn () => (), add req_time' req requests')
+          else (request_event req, requests')
+        end |> SOME);
 
 
 (* global state *)
@@ -105,7 +115,7 @@
   if Synchronized.timed_access state
     (fn State {requests, ...} => next_time requests)
     (fn st as State {requests, status, manager} =>
-      (case next_event (Time.now ()) requests of
+      (case next_event (Time.now (), ML_Heap.gc_now ()) requests of
         SOME (event, requests') =>
           let
             val _ = Exn.capture event ();
@@ -144,10 +154,10 @@
 
 (* main operations *)
 
-fun request time event =
+fun request {physical} time event =
   Synchronized.change_result state (fn State {requests, status, manager} =>
     let
-      val req = new_request time event;
+      val req = new_request physical time event;
       val requests' = add time req requests;
       val manager' = manager_check manager;
     in (req, make_state (requests', status, manager')) end);
@@ -159,12 +169,13 @@
       val manager' = manager_check manager;
     in (canceled, make_state (requests', status, manager')) end);
 
-val future = Thread_Attributes.uninterruptible (fn _ => fn time =>
-  let
-    val req: request Single_Assignment.var = Single_Assignment.var "req";
-    fun abort () = ignore (cancel (Single_Assignment.await req));
-    val promise: unit future = Future.promise_name "event_timer" abort;
-    val _ = Single_Assignment.assign req (request time (Future.fulfill promise));
-  in promise end);
+fun future physical time =
+  Thread_Attributes.uninterruptible (fn _ => fn () =>
+    let
+      val req: request Single_Assignment.var = Single_Assignment.var "req";
+      fun abort () = ignore (cancel (Single_Assignment.await req));
+      val promise: unit future = Future.promise_name "event_timer" abort;
+      val _ = Single_Assignment.assign req (request physical time (Future.fulfill promise));
+    in promise end) ();
 
 end;

--- a/src/Pure/Concurrent/timeout.ML	Wed Feb 20 21:20:30 2019 +0100
+++ b/src/Pure/Concurrent/timeout.ML	Wed Feb 20 21:54:52 2019 +0100
@@ -23,7 +23,7 @@
       val start = Time.now ();
 
       val request =
-        Event_Timer.request (start + timeout)
+        Event_Timer.request {physical = false} (start + timeout)
           (fn () => Standard_Thread.interrupt_unsynchronized self);
       val result =
         Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();

--- a/src/Pure/ML/ml_heap.ML	Wed Feb 20 21:20:30 2019 +0100
+++ b/src/Pure/ML/ml_heap.ML	Wed Feb 20 21:54:52 2019 +0100
@@ -8,6 +8,7 @@
 sig
   val obj_size: 'a -> int
   val full_gc: unit -> unit
+  val gc_now: unit -> Time.time
   val share_common_data: unit -> unit
   val save_child: string -> unit
 end;
@@ -19,6 +20,8 @@
 
 val full_gc = PolyML.fullGC;
 
+fun gc_now () = #timeGCReal (PolyML.Statistics.getLocalStats ());
+
 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
 
 fun save_child name =

--- a/src/Pure/PIDE/command.ML	Wed Feb 20 21:20:30 2019 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Feb 20 21:54:52 2019 +0100
@@ -483,7 +483,7 @@
   in
     (case delay of
       NONE => fork ()
-    | SOME d => ignore (Event_Timer.request (Time.now () + d) fork))
+    | SOME d => ignore (Event_Timer.request {physical = true} (Time.now () + d) fork))
   end;
 
 fun run_print execution_id (print as Print {exec_id, print_process, ...}) =

--- 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