src/Pure/PIDE/document.ML

 val timing = Unsynchronized.ref false;
 fun timeit msg e = cond_timeit (! timing) msg e;
 
 
 
-
-
-
 (** document structure **)
 
 fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
 fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
 

 type blob_digest = (string * string option) Exn.result;  (*file node name, raw digest*)
 
 type execution =
  {version_id: Document_ID.version,  (*static version id*)
   execution_id: Document_ID.execution,  (*dynamic execution id*)
-  delay_request: unit future,  (*pending event timer request*)
-  frontier: Future.task Symtab.table};  (*node name -> running execution task*)
+  delay_request: unit future};  (*pending event timer request*)
 
 val no_execution: execution =
-  {version_id = Document_ID.none, execution_id = Document_ID.none,
-   delay_request = Future.value (), frontier = Symtab.empty};
-
-fun new_execution version_id delay_request frontier : execution =
-  {version_id = version_id, execution_id = Execution.start (),
-   delay_request = delay_request, frontier = frontier};
+  {version_id = Document_ID.none,
+   execution_id = Document_ID.none,
+   delay_request = Future.value ()};
+
+fun new_execution version_id delay_request : execution =
+  {version_id = version_id,
+   execution_id = Execution.start (),
+   delay_request = delay_request};
 
 abstype state = State of
  {versions: version Inttab.table,  (*version id -> document content*)
   blobs: (SHA1.digest * string list) Symtab.table,  (*raw digest -> digest, lines*)
   commands: (string * blob_digest list * Token.T list lazy) Inttab.table,

 
 
 (* document versions *)
 
 fun define_version version_id version =
-  map_state (fn (versions, blobs, commands, {delay_request, frontier, ...}) =>
+  map_state (fn (versions, blobs, commands, {delay_request, ...}) =>
     let
       val versions' = Inttab.update_new (version_id, version) versions
         handle Inttab.DUP dup => err_dup "document version" dup;
-      val execution' = new_execution version_id delay_request frontier;
+      val execution' = new_execution version_id delay_request;
     in (versions', blobs, commands, execution') end);
 
 fun the_version (State {versions, ...}) version_id =
   (case Inttab.lookup versions version_id of
     NONE => err_undef "document version" version_id

 (* document execution *)
 
 fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
   timeit "Document.start_execution" (fn () =>
     let
-      val {version_id, execution_id, delay_request, frontier} = execution;
+      val {version_id, execution_id, delay_request} = execution;
 
       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 new_tasks =
+      val _ =
         nodes_of (the_version state version_id) |> String_Graph.schedule
           (fn deps => fn (name, node) =>
             if visible_node node orelse pending_result node then
               let
-                val more_deps =
-                  Future.task_of delay_request' :: the_list (Symtab.lookup frontier name);
                 fun body () =
                   iterate_entries (fn (_, opt_exec) => fn () =>
                     (case opt_exec of
                       SOME exec =>
                         if Execution.is_running execution_id

                         else NONE
                     | NONE => NONE)) node ()
                   handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn;
                 val future =
                   (singleton o Future.forks)
-                    {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
-                      deps = more_deps @ map #2 (maps #2 deps),
-                      pri = 0, interrupts = false} body;
-              in [(name, Future.task_of future)] end
+                   {name = "theory:" ^ name,
+                    group = SOME (Future.new_group NONE),
+                    deps = Future.task_of delay_request' :: maps #2 deps,
+                    pri = 0, interrupts = false} body;
+              in [Future.task_of future] end
             else []);
-      val frontier' = (fold o fold) Symtab.update new_tasks frontier;
       val execution' =
-        {version_id = version_id, execution_id = execution_id,
-         delay_request = delay_request', frontier = frontier'};
+        {version_id = version_id, execution_id = execution_id, delay_request = delay_request'};
     in (versions, blobs, commands, execution') end));
 
 
 
 (** document update **)