src/Pure/PIDE/document.ML
changeset 52798 9d3c9862d1dd
parent 52797 0d6f2a87d1a5
child 52808 143f225e50f5
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Jul 30 16:22:07 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Jul 30 18:19:16 2013 +0200
     1.3 @@ -204,13 +204,16 @@
     1.4  type execution =
     1.5   {version_id: Document_ID.version,  (*static version id*)
     1.6    execution_id: Document_ID.execution,  (*dynamic execution id*)
     1.7 +  delay_request: unit future,  (*pending event timer request*)
     1.8    frontier: Future.task Symtab.table};  (*node name -> running execution task*)
     1.9  
    1.10  val no_execution: execution =
    1.11 -  {version_id = Document_ID.none, execution_id = Document_ID.none, frontier = Symtab.empty};
    1.12 +  {version_id = Document_ID.none, execution_id = Document_ID.none,
    1.13 +   delay_request = Future.value (), frontier = Symtab.empty};
    1.14  
    1.15 -fun new_execution version_id frontier : execution =
    1.16 -  {version_id = version_id, execution_id = Execution.start (), frontier = frontier};
    1.17 +fun new_execution version_id delay_request frontier : execution =
    1.18 +  {version_id = version_id, execution_id = Execution.start (),
    1.19 +   delay_request = delay_request, frontier = frontier};
    1.20  
    1.21  abstype state = State of
    1.22   {versions: version Inttab.table,  (*version id -> document content*)
    1.23 @@ -231,11 +234,11 @@
    1.24  (* document versions *)
    1.25  
    1.26  fun define_version version_id version =
    1.27 -  map_state (fn (versions, commands, {frontier, ...}) =>
    1.28 +  map_state (fn (versions, commands, {delay_request, frontier, ...}) =>
    1.29      let
    1.30        val versions' = Inttab.update_new (version_id, version) versions
    1.31          handle Inttab.DUP dup => err_dup "document version" dup;
    1.32 -      val execution' = new_execution version_id frontier;
    1.33 +      val execution' = new_execution version_id delay_request frontier;
    1.34      in (versions', commands, execution') end);
    1.35  
    1.36  fun the_version (State {versions, ...}) version_id =
    1.37 @@ -299,15 +302,21 @@
    1.38  fun start_execution state = state |> map_state (fn (versions, commands, execution) =>
    1.39    timeit "Document.start_execution" (fn () =>
    1.40      let
    1.41 -      val {version_id, execution_id, frontier} = execution;
    1.42 +      val {version_id, execution_id, delay_request, frontier} = execution;
    1.43 +
    1.44 +      val delay = seconds (Options.default_real "editor_execution_delay");
    1.45        val pri = Options.default_int "editor_execution_priority";
    1.46  
    1.47 +      val _ = Future.cancel delay_request;
    1.48 +      val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay));
    1.49 +
    1.50        val new_tasks =
    1.51          nodes_of (the_version state version_id) |> String_Graph.schedule
    1.52            (fn deps => fn (name, node) =>
    1.53              if visible_node node orelse pending_result node then
    1.54                let
    1.55 -                val former_task = Symtab.lookup frontier name;
    1.56 +                val more_deps =
    1.57 +                  Future.task_of delay_request' :: the_list (Symtab.lookup frontier name);
    1.58                  fun body () =
    1.59                    iterate_entries (fn (_, opt_exec) => fn () =>
    1.60                      (case opt_exec of
    1.61 @@ -320,12 +329,14 @@
    1.62                  val future =
    1.63                    (singleton o Future.forks)
    1.64                      {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    1.65 -                      deps = the_list former_task @ map #2 (maps #2 deps),
    1.66 +                      deps = more_deps @ map #2 (maps #2 deps),
    1.67                        pri = pri, interrupts = false} body;
    1.68                in [(name, Future.task_of future)] end
    1.69              else []);
    1.70        val frontier' = (fold o fold) Symtab.update new_tasks frontier;
    1.71 -      val execution' = {version_id = version_id, execution_id = execution_id, frontier = frontier'};
    1.72 +      val execution' =
    1.73 +        {version_id = version_id, execution_id = execution_id,
    1.74 +         delay_request = delay_request', frontier = frontier'};
    1.75      in (versions, commands, execution') end));
    1.76  
    1.77