1.1 --- a/src/Pure/PIDE/document.ML	Mon Jul 29 16:01:05 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Jul 29 16:52:04 2013 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    val init_state: state
     1.5    val define_command: Document_ID.command -> string -> string -> state -> state
     1.6    val remove_versions: Document_ID.version list -> state -> state
     1.7 -  val start_execution: state -> unit
     1.8 +  val start_execution: state -> state
     1.9    val timing: bool Unsynchronized.ref
    1.10    val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
    1.11      Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
    1.12 @@ -196,10 +196,16 @@
    1.13  
    1.14  (** main state -- document structure and execution process **)
    1.15  
    1.16 -type execution = {version_id: Document_ID.version, execution_id: Document_ID.execution};
    1.17 +type execution =
    1.18 + {version_id: Document_ID.version,  (*static version id*)
    1.19 +  execution_id: Document_ID.execution,  (*dynamic execution id*)
    1.20 +  frontier: Future.task Symtab.table};  (*node name -> running execution task*)
    1.21  
    1.22 -val no_execution = {version_id = Document_ID.none, execution_id = Document_ID.none};
    1.23 -fun new_execution version_id = {version_id = version_id, execution_id = Execution.start ()};
    1.24 +val no_execution: execution =
    1.25 +  {version_id = Document_ID.none, execution_id = Document_ID.none, frontier = Symtab.empty};
    1.26 +
    1.27 +fun new_execution version_id frontier : execution =
    1.28 +  {version_id = version_id, execution_id = Execution.start (), frontier = frontier};
    1.29  
    1.30  abstype state = State of
    1.31   {versions: version Inttab.table,  (*version id -> document content*)
    1.32 @@ -216,17 +222,15 @@
    1.33  val init_state =
    1.34    make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, no_execution);
    1.35  
    1.36 -fun execution_of (State {execution, ...}) = execution;
    1.37 -
    1.38  
    1.39  (* document versions *)
    1.40  
    1.41  fun define_version version_id version =
    1.42 -  map_state (fn (versions, commands, _) =>
    1.43 +  map_state (fn (versions, commands, {frontier, ...}) =>
    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;
    1.48 +      val execution' = new_execution version_id frontier;
    1.49      in (versions', commands, execution') end);
    1.50  
    1.51  fun the_version (State {versions, ...}) version_id =
    1.52 @@ -287,29 +291,37 @@
    1.53  
    1.54  (* document execution *)
    1.55  
    1.56 -fun start_execution state =
    1.57 +fun start_execution state = state |> map_state (fn (versions, commands, execution) =>
    1.58    let
    1.59 -    val {version_id, execution_id} = execution_of state;
    1.60 +    val {version_id, execution_id, frontier} = execution;
    1.61      val pri = Options.default_int "editor_execution_priority";
    1.62 -    val _ =
    1.63 +
    1.64 +    val new_tasks =
    1.65        if Execution.is_running execution_id then
    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 -              (singleton o Future.forks)
    1.70 -                {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    1.71 -                  deps = map (Future.task_of o #2) deps, pri = pri, interrupts = false}
    1.72 -                (fn () =>
    1.73 -                  iterate_entries (fn (_, opt_exec) => fn () =>
    1.74 -                    (case opt_exec of
    1.75 -                      SOME exec =>
    1.76 -                        if Execution.is_running execution_id
    1.77 -                        then SOME (Command.exec execution_id exec)
    1.78 -                        else NONE
    1.79 -                    | NONE => NONE)) node ())
    1.80 -            else Future.value ())
    1.81 +              let
    1.82 +                val former_task = Symtab.lookup frontier name;
    1.83 +                val future =
    1.84 +                  (singleton o Future.forks)
    1.85 +                    {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    1.86 +                      deps = the_list former_task @ map #2 (maps #2 deps),
    1.87 +                      pri = pri, interrupts = false}
    1.88 +                    (fn () =>
    1.89 +                      iterate_entries (fn (_, opt_exec) => fn () =>
    1.90 +                        (case opt_exec of
    1.91 +                          SOME exec =>
    1.92 +                            if Execution.is_running execution_id
    1.93 +                            then SOME (Command.exec execution_id exec)
    1.94 +                            else NONE
    1.95 +                        | NONE => NONE)) node ());
    1.96 +              in [(name, Future.task_of future)] end
    1.97 +            else [])
    1.98        else [];
    1.99 -  in () end;
   1.100 +    val frontier' = (fold o fold) Symtab.update new_tasks frontier;
   1.101 +    val execution' = {version_id = version_id, execution_id = execution_id, frontier = frontier'};
   1.102 +  in (versions, commands, execution') end);
   1.103  
   1.104  
   1.105