# HG changeset patch # User wenzelm # Date 1550696092 -3600 # Node ID 1bea05713dde80c3ea3511f1906c68d3316482f7 # Parent 183c345b063e0f9e2ba160d26192923744a2ae6a physical vs. logical events, the latter takes GC time into account; Timeout.apply is based on logical ML time; diff -r 183c345b063e -r 1bea05713dde src/Pure/Concurrent/event_timer.ML --- 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; diff -r 183c345b063e -r 1bea05713dde src/Pure/Concurrent/timeout.ML --- 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)) (); diff -r 183c345b063e -r 1bea05713dde src/Pure/ML/ml_heap.ML --- 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 = diff -r 183c345b063e -r 1bea05713dde src/Pure/PIDE/command.ML --- 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, ...}) = diff -r 183c345b063e -r 1bea05713dde 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