# HG changeset patch # User wenzelm # Date 1333658032 -7200 # Node ID 193251980a731b56d2a02c0705868b8d7cb25953 # Parent ca5eb90cc84a8651a9b9dd6c071ad181a7e9965c more scalable execute/update: avoid redundant traversal of invisible/finished nodes; tuned; diff -r ca5eb90cc84a -r 193251980a73 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Apr 05 14:34:54 2012 +0200 +++ b/src/Pure/PIDE/document.ML Thu Apr 05 22:33:52 2012 +0200 @@ -27,10 +27,10 @@ val define_command: command_id -> string -> string -> state -> state val discontinue_execution: state -> unit val cancel_execution: state -> Future.task list + val execute: version_id -> state -> state val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state val update: version_id -> version_id -> edit list -> state -> ((command_id * exec_id option) list * (string * command_id option) list) * state - val execute: version_id -> state -> state val remove_versions: version_id list -> state -> state val state: unit -> state val change_state: (state -> state) -> unit @@ -111,6 +111,10 @@ map_node (fn (touched, header, _, entries, last_exec, result) => (touched, header, make_perspective ids, entries, last_exec, result)); +val visible_command = #1 o get_perspective; +val visible_last = #2 o get_perspective; +val visible_node = is_some o visible_last + fun map_entries f = map_node (fn (touched, header, perspective, entries, last_exec, result) => (touched, header, perspective, f entries, last_exec, result)); @@ -293,7 +297,7 @@ (* document execution *) -fun discontinue_execution (State {execution = (_, _, running), ...}) = running := false; +fun discontinue_execution (State {execution = (_, _, running), ...}) = running := false; fun cancel_execution (State {execution = (_, group, _), ...}) = Future.cancel_group group; @@ -301,6 +305,49 @@ +(** execute **) + +fun finished_theory node = + (case Exn.capture Command.memo_result (get_result node) of + Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st + | _ => false); + +fun execute version_id state = + state |> map_state (fn (versions, commands, _) => + let + val version = the_version state version_id; + + val group = Future.new_group NONE; + val running = Unsynchronized.ref true; + + fun run _ _ NONE = () + | run node command_id (SOME (_, exec)) = + let + val (_, print) = Command.memo_eval exec; + val _ = + if visible_command node command_id + then ignore (Lazy.future Future.default_params print) + else (); + in () end; + + val _ = + nodes_of version |> Graph.schedule + (fn deps => fn (name, node) => + if not (visible_node node) andalso finished_theory node then + Future.value () + else + (singleton o Future.forks) + {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), + deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} + (fn () => + iterate_entries (fn ((_, id), exec) => fn () => + if ! running then SOME (run node id exec) else NONE) node ())); + + in (versions, commands, (version_id, group, running)) end); + + + + (** update **) (* perspective *) @@ -320,11 +367,14 @@ fun make_required nodes = let val all_visible = - Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes [] - |> Graph.all_preds nodes; + Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes [] + |> Graph.all_preds nodes + |> map (rpair ()) |> Symtab.make; + val required = - fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ())) - all_visible Symtab.empty; + Symtab.fold (fn (a, ()) => + exists (Symtab.defined all_visible) (Graph.immediate_succs nodes a) ? + Symtab.update (a, ())) all_visible Symtab.empty; in Symtab.defined required end; fun init_theory deps node = @@ -419,7 +469,7 @@ val updated = nodes |> Graph.schedule (fn deps => fn (name, node) => - if is_touched node orelse is_required name then + if is_touched node orelse is_required name andalso not (finished_theory node) then let val node0 = node_of old_version name; fun init () = init_theory deps node; @@ -432,7 +482,7 @@ (fn () => let val required = is_required name; - val last_visible = #2 (get_perspective node); + val last_visible = visible_last node; val (common, (visible, initial)) = last_common state last_visible node0 node; val common_command_exec = the_default_entry node common; @@ -480,39 +530,6 @@ end; -(* execute *) - -fun execute version_id state = - state |> map_state (fn (versions, commands, _) => - let - val version = the_version state version_id; - - val group = Future.new_group NONE; - val running = Unsynchronized.ref true; - - fun run _ _ NONE = () - | run node command_id (SOME (_, exec)) = - let - val (_, print) = Command.memo_eval exec; - val _ = - if #1 (get_perspective node) command_id - then ignore (Lazy.future Future.default_params print) - else (); - in () end; - - val _ = - nodes_of version |> Graph.schedule - (fn deps => fn (name, node) => - (singleton o Future.forks) - {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), - deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} - (fn () => - iterate_entries (fn ((_, id), exec) => fn () => - if ! running then SOME (run node id exec) else NONE) node ())); - - in (versions, commands, (version_id, group, running)) end); - - (* remove versions *) fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>