changeset 62826 | eb94e570c1a4 |
parent 62505 | 9e2a65912111 |
child 62895 | 54c2abe7e9a4 |
--- a/src/Pure/PIDE/document.ML Sat Apr 02 23:14:08 2016 +0200 +++ b/src/Pure/PIDE/document.ML Sat Apr 02 23:29:05 2016 +0200 @@ -464,7 +464,7 @@ val delay = seconds (Options.default_real "editor_execution_delay"); val _ = Future.cancel delay_request; - val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay)); + val delay_request' = Event_Timer.future (Time.now () + delay); fun finished_import (name, (node, _)) = finished_result node orelse is_some (loaded_theory name);