# HG changeset patch
# User wenzelm
# Date 1314444366 -7200
# Node ID da5f0af32c1b02583b4a4d8aca36aecdf72f0de5
# Parent  ba8f24f7156e17c4af497abf02f04ab77d640310
more precise treatment of nodes that are fully required for partially visible ones;

diff -r ba8f24f7156e -r da5f0af32c1b src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Aug 27 12:22:24 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Aug 27 13:26:06 2011 +0200
@@ -215,9 +215,7 @@
         in Graph.map_node name (set_header header') nodes3 end
         |> touch_node name
     | Perspective perspective =>
-        nodes
-        |> update_node name (set_perspective perspective)
-        |> touch_node name (* FIXME more precise!?! *));
+        update_node name (set_perspective perspective) nodes);
 
 end;
 
@@ -382,7 +380,7 @@
 
 fun last_common last_visible node0 node =
   let
-    fun get_common ((prev, id), exec) (found, (result, visible)) =
+    fun get_common ((prev, id), exec) (found, (_, visible)) =
       if found then NONE
       else
         let val found' = is_none exec orelse exec <> lookup_entry node0 id
@@ -403,6 +401,16 @@
       |> pair command_id';
   in ((exec_id', exec') :: execs, exec') end;
 
+fun make_required nodes =
+  let
+    val all_visible =
+      Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes []
+      |> Graph.all_preds nodes;
+    val required =
+      fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ()))
+        all_visible Symtab.empty;
+  in Symtab.defined required end;
+
 fun init_theory deps name node =
   let
     val (thy_name, imports, uses) = Exn.release (get_header node);
@@ -428,10 +436,14 @@
     val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
     val new_version = fold edit_nodes edits old_version;
 
+    val nodes = nodes_of new_version;
+    val is_required = make_required nodes;
+
     val updated =
-      nodes_of new_version |> Graph.schedule
+      nodes |> Graph.schedule
         (fn deps => fn (name, node) =>
-          if not (is_touched node) then Future.value (([], [], []), node)
+          if not (is_touched node orelse is_required name)
+          then Future.value (([], [], []), node)
           else
             let
               val node0 = node_of old_version name;
@@ -442,15 +454,16 @@
                   deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
                 (fn () =>
                   let
+                    val required = is_required name;
                     val last_visible = #2 (get_perspective node);
                     val (common, visible) = last_common last_visible node0 node;
                     val common_exec = the_exec state (the_default_entry node common);
 
                     val (execs, exec) = ([], common_exec) |>
-                      visible ?
+                      (visible orelse required) ?
                         iterate_entries (after_entry node common)
                           (fn ((prev, id), _) => fn res =>
-                            if prev = last_visible then NONE
+                            if not required andalso prev = last_visible then NONE
                             else SOME (new_exec state init id res)) node;
 
                     val no_execs =