tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;

--- a/src/Pure/PIDE/document.ML	Wed Aug 24 16:49:48 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Aug 24 17:14:31 2011 +0200
@@ -62,18 +62,20 @@
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
 abstype node = Node of
- {header: node_header,
+ {touched: bool,
+  header: node_header,
   perspective: perspective,
   entries: exec_id option Entries.T,  (*command entries with excecutions*)
   result: Toplevel.state lazy}
 and version = Version of node Graph.T  (*development graph wrt. static imports*)
 with
 
-fun make_node (header, perspective, entries, result) =
-  Node {header = header, perspective = perspective, entries = entries, result = result};
+fun make_node (touched, header, perspective, entries, result) =
+  Node {touched = touched, header = header, perspective = perspective,
+    entries = entries, result = result};
 
-fun map_node f (Node {header, perspective, entries, result}) =
-  make_node (f (header, perspective, entries, result));
+fun map_node f (Node {touched, header, perspective, entries, result}) =
+  make_node (f (touched, header, perspective, entries, result));
 
 fun make_perspective ids : perspective =
   (Inttab.defined (Inttab.make (map (rpair ()) ids)), ids);
@@ -83,30 +85,39 @@
 val no_result = Lazy.value Toplevel.toplevel;
 
 val empty_node =
-  make_node (Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result);
+  make_node (false, Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result);
 
 val clear_node =
-  map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, no_result));
+  map_node (fn (_, header, _, _, _) => (false, header, no_perspective, Entries.empty, no_result));
 
 
 (* basic components *)
 
+fun get_touched (Node {touched, ...}) = touched;
+fun set_touched touched =
+  map_node (fn (_, header, perspective, entries, result) =>
+    (touched, header, perspective, entries, result));
+
 fun get_header (Node {header, ...}) = header;
 fun set_header header =
-  map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
+  map_node (fn (touched, _, perspective, entries, result) =>
+    (touched, header, perspective, entries, result));
 
 fun get_perspective (Node {perspective, ...}) = perspective;
 fun set_perspective ids =
-  map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result));
+  map_node (fn (touched, header, _, entries, result) =>
+    (touched, header, make_perspective ids, entries, result));
 
-fun map_entries f (Node {header, perspective, entries, result}) =
-  make_node (header, perspective, f entries, result);
+fun map_entries f =
+  map_node (fn (touched, header, perspective, entries, result) =>
+    (touched, header, perspective, f entries, result));
 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
 
 fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
 fun set_result result =
-  map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
+  map_node (fn (touched, header, perspective, entries, _) =>
+    (touched, header, perspective, entries, result));
 
 fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
 fun default_node name = Graph.default_node (name, empty_node);
@@ -148,23 +159,29 @@
 fun nodes_of (Version nodes) = nodes;
 val node_of = get_node o nodes_of;
 
+local
+
 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)))
+fun touch_node name nodes =
+  fold (fn desc =>
+      update_node desc (set_touched true) #>
+      desc <> name ? update_node desc (map_entries (reset_after NONE)))
     (Graph.all_succs nodes [name]) nodes;
 
+in
+
 fun edit_nodes (name, node_edit) (Version nodes) =
   Version
     (case node_edit of
       Clear =>
         nodes
         |> update_node name clear_node
-        |> touch_descendants name
+        |> touch_node name
     | Edits edits =>
         nodes
         |> update_node name (edit_node edits)
-        |> touch_descendants name
+        |> touch_node name
     | Header header =>
         let
           val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
@@ -178,10 +195,12 @@
             (header, Graph.add_deps_acyclic (name, parents) nodes2)
               handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
         in Graph.map_node name (set_header header') nodes3 end
-        |> touch_descendants name
+        |> touch_node name
     | Perspective perspective =>
         update_node name (set_perspective perspective) nodes);
 
+end;
+
 fun put_node (name, node) (Version nodes) =
   Version (update_node name (K node) nodes);
 
@@ -386,29 +405,32 @@
     val updates =
       nodes_of new_version |> Graph.schedule
         (fn deps => fn (name, node) =>
-          (case first_entry NONE (is_changed (node_of old_version name)) node of
-            NONE => Future.value (([], [], []), node)
-          | SOME ((prev, id), _) =>
-              let
-                fun init () = init_theory deps name node;
-              in
-                (singleton o Future.forks)
-                  {name = "Document.edit", group = NONE,
-                    deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
-                  (fn () =>
-                    let
-                      val prev_exec =
-                        (case prev of
-                          NONE => no_id
-                        | SOME prev_id => the_default no_id (the_entry node prev_id));
-                      val (assigns, execs, last_exec) =
-                        fold_entries (SOME id) (new_exec state init o #2 o #1)
-                          node ([], [], #2 (the_exec state prev_exec));
-                      val node' = node
-                        |> fold update_entry assigns
-                        |> set_result (Lazy.map #1 last_exec);
-                    in ((assigns, execs, [(name, node')]), node') end)
-              end))
+          if not (get_touched node) then Future.value (([], [], []), node)
+          else
+            (case first_entry NONE (is_changed (node_of old_version name)) node of
+              NONE => Future.value (([], [], []), set_touched false node)
+            | SOME ((prev, id), _) =>
+                let
+                  fun init () = init_theory deps name node;
+                in
+                  (singleton o Future.forks)
+                    {name = "Document.edit", group = NONE,
+                      deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
+                    (fn () =>
+                      let
+                        val prev_exec =
+                          (case prev of
+                            NONE => no_id
+                          | SOME prev_id => the_default no_id (the_entry node prev_id));
+                        val (assigns, execs, last_exec) =
+                          fold_entries (SOME id) (new_exec state init o #2 o #1)
+                            node ([], [], #2 (the_exec state prev_exec));
+                        val node' = node
+                          |> fold update_entry assigns
+                          |> set_result (Lazy.map #1 last_exec)
+                          |> set_touched false;
+                      in ((assigns, execs, [(name, node')]), node') end)
+                end))
       |> Future.joins |> map #1;
 
     val state' = state