# HG changeset patch # User wenzelm # Date 1314198871 -7200 # Node ID 33a5616a757186fa209092c847f92ede9e47e362 # Parent 35d67b2056cc55199bbe3ca392fd71eadced6b55 tuned Document.node: maintain "touched" flag to indicate changes in entries etc.; diff -r 35d67b2056cc -r 33a5616a7571 src/Pure/PIDE/document.ML --- 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