src/Pure/PIDE/document.ML
changeset 59193 59f1591a11cb
parent 59086 94b2690ad494
child 59198 c73933e07c03
     1.1 --- a/src/Pure/PIDE/document.ML	Sun Dec 28 12:37:03 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Dec 28 21:34:45 2014 +0100
     1.3 @@ -37,9 +37,6 @@
     1.4  
     1.5  
     1.6  
     1.7 -
     1.8 -
     1.9 -
    1.10  (** document structure **)
    1.11  
    1.12  fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
    1.13 @@ -285,16 +282,17 @@
    1.14  type execution =
    1.15   {version_id: Document_ID.version,  (*static version id*)
    1.16    execution_id: Document_ID.execution,  (*dynamic execution id*)
    1.17 -  delay_request: unit future,  (*pending event timer request*)
    1.18 -  frontier: Future.task Symtab.table};  (*node name -> running execution task*)
    1.19 +  delay_request: unit future};  (*pending event timer request*)
    1.20  
    1.21  val no_execution: execution =
    1.22 -  {version_id = Document_ID.none, execution_id = Document_ID.none,
    1.23 -   delay_request = Future.value (), frontier = Symtab.empty};
    1.24 +  {version_id = Document_ID.none,
    1.25 +   execution_id = Document_ID.none,
    1.26 +   delay_request = Future.value ()};
    1.27  
    1.28 -fun new_execution version_id delay_request frontier : execution =
    1.29 -  {version_id = version_id, execution_id = Execution.start (),
    1.30 -   delay_request = delay_request, frontier = frontier};
    1.31 +fun new_execution version_id delay_request : execution =
    1.32 +  {version_id = version_id,
    1.33 +   execution_id = Execution.start (),
    1.34 +   delay_request = delay_request};
    1.35  
    1.36  abstype state = State of
    1.37   {versions: version Inttab.table,  (*version id -> document content*)
    1.38 @@ -318,11 +316,11 @@
    1.39  (* document versions *)
    1.40  
    1.41  fun define_version version_id version =
    1.42 -  map_state (fn (versions, blobs, commands, {delay_request, frontier, ...}) =>
    1.43 +  map_state (fn (versions, blobs, commands, {delay_request, ...}) =>
    1.44      let
    1.45        val versions' = Inttab.update_new (version_id, version) versions
    1.46          handle Inttab.DUP dup => err_dup "document version" dup;
    1.47 -      val execution' = new_execution version_id delay_request frontier;
    1.48 +      val execution' = new_execution version_id delay_request;
    1.49      in (versions', blobs, commands, execution') end);
    1.50  
    1.51  fun the_version (State {versions, ...}) version_id =
    1.52 @@ -408,20 +406,18 @@
    1.53  fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
    1.54    timeit "Document.start_execution" (fn () =>
    1.55      let
    1.56 -      val {version_id, execution_id, delay_request, frontier} = execution;
    1.57 +      val {version_id, execution_id, delay_request} = execution;
    1.58  
    1.59        val delay = seconds (Options.default_real "editor_execution_delay");
    1.60  
    1.61        val _ = Future.cancel delay_request;
    1.62        val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay));
    1.63  
    1.64 -      val new_tasks =
    1.65 +      val _ =
    1.66          nodes_of (the_version state version_id) |> String_Graph.schedule
    1.67            (fn deps => fn (name, node) =>
    1.68              if visible_node node orelse pending_result node then
    1.69                let
    1.70 -                val more_deps =
    1.71 -                  Future.task_of delay_request' :: the_list (Symtab.lookup frontier name);
    1.72                  fun body () =
    1.73                    iterate_entries (fn (_, opt_exec) => fn () =>
    1.74                      (case opt_exec of
    1.75 @@ -433,15 +429,14 @@
    1.76                    handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn;
    1.77                  val future =
    1.78                    (singleton o Future.forks)
    1.79 -                    {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    1.80 -                      deps = more_deps @ map #2 (maps #2 deps),
    1.81 -                      pri = 0, interrupts = false} body;
    1.82 -              in [(name, Future.task_of future)] end
    1.83 +                   {name = "theory:" ^ name,
    1.84 +                    group = SOME (Future.new_group NONE),
    1.85 +                    deps = Future.task_of delay_request' :: maps #2 deps,
    1.86 +                    pri = 0, interrupts = false} body;
    1.87 +              in [Future.task_of future] end
    1.88              else []);
    1.89 -      val frontier' = (fold o fold) Symtab.update new_tasks frontier;
    1.90        val execution' =
    1.91 -        {version_id = version_id, execution_id = execution_id,
    1.92 -         delay_request = delay_request', frontier = frontier'};
    1.93 +        {version_id = version_id, execution_id = execution_id, delay_request = delay_request'};
    1.94      in (versions, blobs, commands, execution') end));
    1.95  
    1.96