src/Pure/PIDE/document.ML
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);