touch descendants of edited nodes;
more precise handling of Graph exceptions;

--- a/src/Pure/General/graph.ML	Mon Aug 15 21:05:30 2011 +0200
+++ b/src/Pure/General/graph.ML	Mon Aug 15 21:54:32 2011 +0200
@@ -35,19 +35,19 @@
   val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
   val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
   val is_edge: 'a T -> key * key -> bool
-  val add_edge: key * key -> 'a T -> 'a T
-  val del_edge: key * key -> 'a T -> 'a T
+  val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
+  val del_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
     'a T * 'a T -> 'a T                                               (*exception DUP*)
   val irreducible_paths: 'a T -> key * key -> key list list
   val all_paths: 'a T -> key * key -> key list list
   exception CYCLES of key list list
-  val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception CYCLES*)
-  val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)
+  val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception UNDEF | CYCLES*)
+  val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception UNDEF | CYCLES*)
   val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
   val topological_order: 'a T -> key list
-  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
+  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception UNDEF | CYCLES*)
   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
   exception DEP of key * key
   val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list  (*exception DEP*)

--- a/src/Pure/PIDE/document.ML	Mon Aug 15 21:05:30 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Aug 15 21:54:32 2011 +0200
@@ -87,7 +87,8 @@
 
 fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
 fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes;
-fun update_node name f = Graph.default_node (name, empty_node) #> Graph.map_node name f;
+fun default_node name = Graph.default_node (name, empty_node);
+fun update_node name f = default_node name #> Graph.map_node name f;
 
 
 (* node edits and associated executions *)
@@ -126,27 +127,36 @@
 
 fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
 
+fun touch_descendants name nodes =
+  fold (fn desc => desc <> name ? update_node desc (map_entries (reset_after NONE)))
+    (Graph.all_succs nodes [name]) nodes;
+
 fun edit_nodes (name, node_edit) (Version nodes) =
   Version
-    (case node_edit of
-      Clear => update_node name clear_node nodes
-    | Edits edits => update_node name (edit_node edits) nodes
-    | Header header =>
-        let
-          val node = get_node nodes name;
-          val nodes' = Graph.new_node (name, node) (remove_node name nodes);
-          val parents =
-            (case header of Exn.Res (_, parents, _) => parents | _ => [])
-            |> filter (can (Graph.get_node nodes'));
-          val (header', nodes'') =
-            (header, Graph.add_deps_acyclic (name, parents) nodes')
-              handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes');
-        in Graph.map_node name (set_header header') nodes'' end);
+    (touch_descendants name
+      (case node_edit of
+        Clear => update_node name clear_node nodes
+      | Edits edits =>
+          nodes
+          |> update_node name (edit_node edits)
+      | Header header =>
+          let
+            val node = get_node nodes name;
+            val nodes' = Graph.new_node (name, node) (remove_node name nodes);
+            val parents =
+              (case header of Exn.Res (_, parents, _) => parents | _ => [])
+              |> filter (can (Graph.get_node nodes'));
+            val (header', nodes'') =
+              (header, Graph.add_deps_acyclic (name, parents) nodes')
+                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes')
+                  | Graph.UNDEF d => (Exn.Exn (ERROR ("Undefined theory entry: " ^ quote d)), nodes')
+          in
+            nodes''
+            |> Graph.map_node name (set_header header')
+          end));
 
-fun put_node (name, node) (Version nodes) =
-  Version (nodes
-    |> Graph.default_node (name, empty_node)
-    |> Graph.map_node name (K node));
+fun def_node name (Version nodes) = Version (default_node name nodes);
+fun put_node (name, node) (Version nodes) = Version (update_node name (K node) nodes);
 
 end;
 
@@ -321,7 +331,10 @@
   let
     val old_version = the_version state old_id;
     val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
-    val new_version = fold edit_nodes edits old_version;
+    val new_version =
+      old_version
+      |> fold (def_node o #1) edits
+      |> fold edit_nodes edits;
 
     val updates =
       nodes_of new_version |> Graph.schedule