# HG changeset patch # User wenzelm # Date 1373385518 -7200 # Node ID 52a0eacf04d1a17e3495baa829c24148c3148bd5 # Parent b04cbc49bdcfacd5b40d3be47632005dd2f9fa4b more formal type assign_update: avoid duplicate results and redundant update of global State.execs; diff -r b04cbc49bdcf -r 52a0eacf04d1 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Tue Jul 09 16:32:51 2013 +0200 +++ b/src/Pure/PIDE/command.ML Tue Jul 09 17:58:38 2013 +0200 @@ -13,7 +13,7 @@ type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process} type exec = eval * print list val no_exec: exec - val exec_ids: exec -> Document_ID.exec list + val exec_ids: exec option -> Document_ID.exec list val read: (unit -> theory) -> Token.T list -> Toplevel.transition val eval: (unit -> theory) -> Token.T list -> eval -> eval val print: string -> eval -> print list @@ -90,7 +90,8 @@ type exec = eval * print list; val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []); -fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints; +fun exec_ids (NONE: exec option) = [] + | exec_ids (SOME ({exec_id, ...}, prints)) = exec_id :: map #exec_id prints; (* read *) diff -r b04cbc49bdcf -r 52a0eacf04d1 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Tue Jul 09 16:32:51 2013 +0200 +++ b/src/Pure/PIDE/document.ML Tue Jul 09 17:58:38 2013 +0200 @@ -108,6 +108,12 @@ fun set_result result = map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result)); +fun changed_result node node' = + (case (get_result node, get_result node') of + (SOME eval, SOME eval') => #exec_id eval <> #exec_id eval' + | (NONE, NONE) => false + | _ => true); + fun finished_theory node = (case Exn.capture (Command.eval_result_state o the) (get_result node) of Exn.Res st => can (Toplevel.end_theory Position.none) st @@ -144,11 +150,9 @@ fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id)) | the_default_entry _ NONE = (Document_ID.none, Command.no_exec); -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 assign_entry (command_id, exec) node = + if is_none (Entries.lookup (get_entries node) command_id) then node + else map_entries (Entries.update (command_id, exec)) node; fun reset_after id entries = (case Entries.get_after entries id of @@ -277,6 +281,9 @@ end; + +(* remove_versions *) + fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) => let val _ = @@ -327,6 +334,25 @@ (** document update **) +(* exec state assignment *) + +type assign_update = Command.exec option Inttab.table; (*command id -> exec*) + +val assign_update_empty: assign_update = Inttab.empty; +fun assign_update_null (tab: assign_update) = Inttab.is_empty tab; +fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id; +fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node; + +fun assign_update_new upd (tab: assign_update) = + Inttab.update_new upd tab + handle Inttab.DUP dup => err_dup "exec state assignment" dup; + +fun assign_update_result (tab: assign_update) = + Inttab.fold (fn (command_id, exec) => cons (command_id, Command.exec_ids exec)) tab []; + + +(* update *) + val timing = Unsynchronized.ref false; fun timeit msg e = cond_timeit (! timing) msg e; @@ -405,19 +431,22 @@ fun illegal_init _ = error "Illegal theory header after end of theory"; -fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) = +fun new_exec state proper_init command_visible command_id' (assign_update, command_exec, init) = if not proper_init andalso is_none init then NONE else let val (_, (eval, _)) = command_exec; val (command_name, span) = the_command state command_id' ||> Lazy.force; - val init' = if Keyword.is_theory_begin command_name then NONE else init; + val eval' = Command.eval (fn () => the_default illegal_init init span) span eval; val prints' = if command_visible then Command.print command_name eval' else []; - val command_exec' = (command_id', (eval', prints')); - in SOME (command_exec' :: execs, command_exec', init') end; + val exec' = (eval', prints'); -fun update_prints state node command_id = + val assign_update' = assign_update_new (command_id', SOME exec') assign_update; + val init' = if Keyword.is_theory_begin command_name then NONE else init; + in SOME (assign_update', (command_id', (eval', prints')), init') end; + +fun update_prints state node command_id assign_update = (case the_entry node command_id of SOME (eval, prints) => let @@ -429,10 +458,10 @@ SOME print => if Command.stable_print print then print else new_print | NONE => new_print)); in - if eq_list (op = o pairself #exec_id) (prints, prints') then NONE - else SOME (command_id, (eval, prints')) + if eq_list (op = o pairself #exec_id) (prints, prints') then assign_update + else assign_update_new (command_id, SOME (eval, prints')) assign_update end - | NONE => NONE); + | NONE => assign_update); in @@ -454,10 +483,10 @@ (fn () => let val imports = map (apsnd Future.join) deps; - val changed_imports = exists (#4 o #1 o #2) imports; + val imports_changed = exists (#3 o #1 o #2) imports; val node_required = is_required name; in - if changed_imports orelse AList.defined (op =) edits name orelse + if imports_changed orelse AList.defined (op =) edits name orelse not (stable_entries node) orelse not (finished_theory node) then let @@ -472,59 +501,54 @@ val last_visible = visible_last node; val (common, (still_visible, initial)) = - if changed_imports then (NONE, (true, true)) + if imports_changed then (NONE, (true, true)) else last_common state last_visible node0 node; + val common_command_exec = the_default_entry node common; val (new_execs, (command_id', (eval', _)), _) = - ([], common_command_exec, if initial then SOME init else NONE) |> - (still_visible orelse node_required) ? + (assign_update_empty, common_command_exec, if initial then SOME init else NONE) + |> (still_visible orelse node_required) ? iterate_entries_after common (fn ((prev, id), _) => fn res => if not node_required andalso prev = last_visible then NONE else new_exec state proper_init (visible_command id) id res) node; val updated_execs = - (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) => - if exists (fn (_, ({exec_id = id', ...}, _)) => id = id') new_execs then I - else append (the_list (update_prints state node id))); + (visible_commands, new_execs) |-> Inttab.fold (fn (command_id, ()) => + not (assign_update_defined new_execs command_id) ? + update_prints state node command_id); - val no_execs = - iterate_entries_after common - (fn ((_, id0), exec0) => fn res => + val assigned_execs = + (node0, updated_execs) |-> iterate_entries_after common + (fn ((_, command_id0), exec0) => fn res => if is_none exec0 then NONE - else if exists (fn (_, ({exec_id = id, ...}, _)) => id0 = id) updated_execs - then SOME res - else SOME (id0 :: res)) node0 []; + else if assign_update_defined updated_execs command_id0 then SOME res + else SOME (assign_update_new (command_id0, NONE) res)); val last_exec = if command_id' = Document_ID.none then NONE else SOME command_id'; val result = - if is_some (after_entry node last_exec) then NONE + if is_none last_exec orelse is_some (after_entry node last_exec) then NONE else SOME eval'; val node' = node - |> fold reset_entry no_execs - |> fold (fn (id, exec) => update_entry id (SOME exec)) updated_execs - |> entries_stable (null updated_execs) + |> assign_update_apply assigned_execs + |> entries_stable (assign_update_null updated_execs) |> set_result result; - val updated_node = - if null no_execs andalso null updated_execs then NONE - else SOME (name, node'); - val changed_result = not (null no_execs) orelse not (null new_execs); - in ((no_execs, updated_execs, updated_node, changed_result), node') end - else (([], [], NONE, false), node) + val assigned_node = + if assign_update_null assigned_execs then NONE else SOME (name, node'); + val result_changed = changed_result node0 node'; + in + ((assign_update_result assigned_execs, assigned_node, result_changed), node') + end + else (([], NONE, false), node) end)) |> Future.joins |> map #1); - val command_execs = - map (rpair []) (maps #1 updated) @ - map (fn (command_id, exec) => (command_id, Command.exec_ids exec)) (maps #2 updated); - val updated_nodes = map_filter #3 updated; - val state' = state - |> define_version new_version_id (fold put_node updated_nodes new_version); - in (command_execs, state') end; + |> define_version new_version_id (fold put_node (map_filter #2 updated) new_version); + in (maps #1 updated, state') end; end; diff -r b04cbc49bdcf -r 52a0eacf04d1 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Jul 09 16:32:51 2013 +0200 +++ b/src/Pure/PIDE/document.scala Tue Jul 09 17:58:38 2013 +0200 @@ -367,20 +367,22 @@ { val version = the_version(id) + def upd(exec_id: Document_ID.Exec, st: Command.State) + : Option[(Document_ID.Exec, Command.State)] = + if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st) + val (changed_commands, new_execs) = ((Nil: List[Command], execs) /: update) { - case ((commands1, execs1), (cmd_id, exec)) => - val st1 = the_static_state(cmd_id) - val command = st1.command - val st0 = command.empty_state - + case ((commands1, execs1), (command_id, exec)) => + val st = the_static_state(command_id) + val command = st.command val commands2 = command :: commands1 val execs2 = exec match { case Nil => execs1 case eval_id :: print_ids => - execs1 + (eval_id -> execs.getOrElse(eval_id, st1)) ++ - print_ids.iterator.map(id => id -> execs.getOrElse(id, st0)) + execs1 ++ upd(eval_id, st) ++ + (for (id <- print_ids; up <- upd(id, command.empty_state)) yield up) } (commands2, execs2) }