src/Pure/PIDE/document.ML
changeset 60198 8483c2883c8c
parent 60027 c42d65e11b6e
child 60880 fa958e24ff24
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Apr 24 19:08:43 2015 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Apr 24 20:33:10 2015 +0200
     1.3 @@ -434,6 +434,21 @@
     1.4  
     1.5  (* document execution *)
     1.6  
     1.7 +fun make_required nodes =
     1.8 +  let
     1.9 +    fun all_preds P =
    1.10 +      String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes []
    1.11 +      |> String_Graph.all_preds nodes
    1.12 +      |> Symtab.make_set;
    1.13 +
    1.14 +    val all_visible = all_preds visible_node;
    1.15 +    val all_required = all_preds required_node;
    1.16 +  in
    1.17 +    Symtab.fold (fn (a, ()) =>
    1.18 +      exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
    1.19 +        Symtab.update (a, ())) all_visible all_required
    1.20 +  end;
    1.21 +
    1.22  fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
    1.23    timeit "Document.start_execution" (fn () =>
    1.24      let
    1.25 @@ -446,10 +461,13 @@
    1.26  
    1.27        fun finished_import (name, (node, _)) =
    1.28          finished_result node orelse is_some (loaded_theory name);
    1.29 +
    1.30 +      val nodes = nodes_of (the_version state version_id);
    1.31 +      val required = make_required nodes;
    1.32        val _ =
    1.33 -        nodes_of (the_version state version_id) |> String_Graph.schedule
    1.34 +        nodes |> String_Graph.schedule
    1.35            (fn deps => fn (name, node) =>
    1.36 -            if visible_node node orelse pending_result node then
    1.37 +            if Symtab.defined required name orelse visible_node node orelse pending_result node then
    1.38                let
    1.39                  fun body () =
    1.40                    (if forall finished_import deps then
    1.41 @@ -498,21 +516,6 @@
    1.42  
    1.43  local
    1.44  
    1.45 -fun make_required nodes =
    1.46 -  let
    1.47 -    fun all_preds P =
    1.48 -      String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes []
    1.49 -      |> String_Graph.all_preds nodes
    1.50 -      |> Symtab.make_set;
    1.51 -
    1.52 -    val all_visible = all_preds visible_node;
    1.53 -    val all_required = all_preds required_node;
    1.54 -  in
    1.55 -    Symtab.fold (fn (a, ()) =>
    1.56 -      exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
    1.57 -        Symtab.update (a, ())) all_visible all_required
    1.58 -  end;
    1.59 -
    1.60  fun init_theory deps node span =
    1.61    let
    1.62      val master_dir = master_directory node;