# HG changeset patch
# User wenzelm
# Date 1429900390 -7200
# Node ID 8483c2883c8c73d94ff05627d5d9de0c821e78ac
# Parent  6e8014342c9d2999dd784f7368e208370a3c20c2
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;

diff -r 6e8014342c9d -r 8483c2883c8c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Apr 24 19:08:43 2015 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Apr 24 20:33:10 2015 +0200
@@ -434,6 +434,21 @@
 
 (* document execution *)
 
+fun make_required nodes =
+  let
+    fun all_preds P =
+      String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes []
+      |> String_Graph.all_preds nodes
+      |> Symtab.make_set;
+
+    val all_visible = all_preds visible_node;
+    val all_required = all_preds required_node;
+  in
+    Symtab.fold (fn (a, ()) =>
+      exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
+        Symtab.update (a, ())) all_visible all_required
+  end;
+
 fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
   timeit "Document.start_execution" (fn () =>
     let
@@ -446,10 +461,13 @@
 
       fun finished_import (name, (node, _)) =
         finished_result node orelse is_some (loaded_theory name);
+
+      val nodes = nodes_of (the_version state version_id);
+      val required = make_required nodes;
       val _ =
-        nodes_of (the_version state version_id) |> String_Graph.schedule
+        nodes |> String_Graph.schedule
           (fn deps => fn (name, node) =>
-            if visible_node node orelse pending_result node then
+            if Symtab.defined required name orelse visible_node node orelse pending_result node then
               let
                 fun body () =
                   (if forall finished_import deps then
@@ -498,21 +516,6 @@
 
 local
 
-fun make_required nodes =
-  let
-    fun all_preds P =
-      String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes []
-      |> String_Graph.all_preds nodes
-      |> Symtab.make_set;
-
-    val all_visible = all_preds visible_node;
-    val all_required = all_preds required_node;
-  in
-    Symtab.fold (fn (a, ()) =>
-      exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
-        Symtab.update (a, ())) all_visible all_required
-  end;
-
 fun init_theory deps node span =
   let
     val master_dir = master_directory node;