# HG changeset patch # User wenzelm # Date 1314386322 -7200 # Node ID c7225307acf23e9588994234212111ed65e81966 # Parent bb42bc83157081824cccea2577595ead9ad22a5e further clarification of Document.updated, based on last_common and after_entry; tuned; diff -r bb42bc831570 -r c7225307acf2 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Aug 26 16:06:58 2011 +0200 +++ b/src/Pure/PIDE/document.ML Fri Aug 26 21:18:42 2011 +0200 @@ -113,7 +113,6 @@ map_node (fn (touched, header, perspective, entries, last_exec, result) => (touched, header, perspective, f entries, last_exec, 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_last_exec (Node {last_exec, ...}) = last_exec; fun set_last_exec last_exec = @@ -140,10 +139,7 @@ type edit = string * node_edit; -fun next_entry (Node {entries, ...}) id = - (case Entries.lookup entries id of - NONE => err_undef "command entry" id - | SOME (_, next) => next); +fun after_entry (Node {entries, ...}) = Entries.get_after entries; fun lookup_entry (Node {entries, ...}) id = (case Entries.lookup entries id of @@ -158,8 +154,11 @@ fun the_default_entry node (SOME id) = the_default no_id (the_entry node id) | the_default_entry _ NONE = no_id; -fun update_entry id exec_id = - map_entries (Entries.update (id, SOME exec_id)); +fun update_entry id exec = + map_entries (Entries.update (id, exec)); + +fun reset_entry id node = + if is_some (lookup_entry node id) then update_entry id NONE node else node; fun reset_after id entries = (case Entries.get_after entries id of @@ -381,6 +380,29 @@ local +fun last_common last_visible node0 node = + let + fun get_common ((prev, id), exec) (found, (result, visible)) = + if found then NONE + else + let val found' = is_none exec orelse exec <> lookup_entry node0 id + in SOME (found', (prev, visible andalso prev <> last_visible)) end; + in #2 (fold_entries NONE get_common node (false, (NONE, true))) end; + +fun new_exec state init command_id' (execs, exec) = + let + val command' = the_command state command_id'; + val exec_id' = new_id (); + val exec' = + snd exec |> Lazy.map (fn (st, _) => + let val tr = + Future.join command' + |> Toplevel.modify_init init + |> Toplevel.put_id (print_id exec_id'); + in run_command tr st end) + |> pair command_id'; + in ((exec_id', exec') :: execs, exec') end; + fun init_theory deps name node = let val (thy_name, imports, uses) = Exn.release (get_header node); @@ -395,26 +417,9 @@ SOME thy => thy | NONE => get_theory (Position.file_only import) - (#2 (Future.join (the (AList.lookup (op =) deps import)))))); + (snd (Future.join (the (AList.lookup (op =) deps import)))))); in Thy_Load.begin_theory dir thy_name imports files parents end; -fun after_perspective node ((prev, _), _) = prev = #2 (get_perspective node); -fun needs_update node0 ((_, id), exec) = is_none exec orelse exec <> lookup_entry node0 id; - -fun new_exec state init command_id' (execs, exec) = - let - val command' = the_command state command_id'; - val exec_id' = new_id (); - val exec' = - snd exec |> Lazy.map (fn (st, _) => - let val tr = - Future.join command' - |> Toplevel.modify_init init - |> Toplevel.put_id (print_id exec_id'); - in run_command tr st end) - |> pair command_id'; - in ((exec_id', exec') :: execs, exec') end; - in fun update (old_id: version_id) (new_id: version_id) edits state = @@ -432,47 +437,41 @@ val node0 = node_of old_version name; fun init () = init_theory deps name node; in - (case first_entry NONE (after_perspective node orf needs_update node0) node of - NONE => Future.value (([], [], []), set_touched false node) - | SOME (entry as ((prev, id), _)) => - (singleton o Future.forks) - {name = "Document.update", group = NONE, - deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} - (fn () => - let - val update_start = - Option.map (#2 o #1) (first_entry (SOME id) (needs_update node0) node); + (singleton o Future.forks) + {name = "Document.update", group = NONE, + deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} + (fn () => + let + 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) = - ([], the_exec state (the_default_entry node prev)) - |> not (after_perspective node entry) ? - fold_entries update_start - (fn entry1 as ((_, id1), _) => fn res => - if after_perspective node entry1 then NONE - else SOME (new_exec state init id1 res)) node; + val (execs, exec) = ([], common_exec) |> + visible ? + fold_entries (after_entry node common) + (fn ((prev, id), _) => fn res => + if prev = last_visible then NONE + else SOME (new_exec state init id res)) node; - val node1 = - fold (fn (exec_id, (command_id, _)) => update_entry command_id exec_id) - execs node; - val last_exec = if #1 exec = no_id then NONE else SOME (#1 exec); - val result = - if is_some last_exec andalso is_none (next_entry node1 (the last_exec)) - then Lazy.map #1 (#2 exec) - else no_result; - val node2 = node1 - |> set_last_exec last_exec - |> set_result result - |> set_touched false; + val no_execs = + fold_entries (after_entry node0 common) + (fn ((_, id0), exec0) => fn res => + if is_none exec0 then NONE + else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res + else SOME (id0 :: res)) node0 []; - val no_execs = - fold_entries update_start - (fn ((_, id0), exec0) => fn res => - if is_none exec0 then NONE - else if is_some (lookup_entry node2 id0) then SOME res - else SOME (id0 :: res)) node0 [] - handle Entries.UNDEFINED _ => []; + val last_exec = if #1 exec = no_id then NONE else SOME (#1 exec); + val result = + if is_some (after_entry node last_exec) then no_result + else Lazy.map #1 (#2 exec); - in ((no_execs, execs, [(name, node2)]), node2) end)) + val node' = node + |> fold reset_entry no_execs + |> fold (fn (exec_id, (id, _)) => update_entry id (SOME exec_id)) execs + |> set_last_exec last_exec + |> set_result result + |> set_touched false; + in ((no_execs, execs, [(name, node')]), node') end) end) |> Future.joins |> map #1;