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