# 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 =