# HG changeset patch # User wenzelm # Date 1334137461 -7200 # Node ID 0dbe6c69eda2d4edbe1e398108ad258b65d9255d # Parent c0e8c98ee50e4ca76a7ac600269eb41ab9d62164 just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update; explicit terminate_execution; tuned source structure; diff -r c0e8c98ee50e -r 0dbe6c69eda2 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Tue Apr 10 23:05:24 2012 +0200 +++ b/src/Pure/PIDE/document.ML Wed Apr 11 11:44:21 2012 +0200 @@ -25,12 +25,12 @@ type state val init_state: state val define_command: command_id -> string -> string -> state -> state + val remove_versions: version_id list -> state -> state val discontinue_execution: state -> unit val cancel_execution: state -> unit - val execute: version_id -> state -> state + val start_execution: state -> unit val update: version_id -> version_id -> edit list -> state -> (command_id * exec_id option) list * state - val remove_versions: version_id list -> state -> state val state: unit -> state val change_state: (state -> state) -> unit end; @@ -144,7 +144,7 @@ NONE => err_undef "command entry" id | SOME (exec, _) => exec); -fun the_default_entry node (SOME id) = (id, (the_default (no_id, no_exec) (the_entry node id))) +fun the_default_entry node (SOME id) = (id, the_default (no_id, no_exec) (the_entry node id)) | the_default_entry _ NONE = (no_id, (no_id, no_exec)); fun update_entry id exec = @@ -220,14 +220,18 @@ make_state (Inttab.make [(no_id, empty_version)], Inttab.empty, (no_id, Future.new_group NONE, Unsynchronized.ref false)); +fun execution_of (State {execution, ...}) = execution; + (* document versions *) fun define_version (id: version_id) version = - map_state (fn (versions, commands, execution) => - let val versions' = Inttab.update_new (id, version) versions - handle Inttab.DUP dup => err_dup "document version" dup - in (versions', commands, execution) end); + map_state (fn (versions, commands, _) => + let + val versions' = Inttab.update_new (id, version) versions + handle Inttab.DUP dup => err_dup "document version" dup; + val execution' = (id, Future.new_group NONE, Unsynchronized.ref true); + in (versions', commands, execution') end); fun the_version (State {versions, ...}) (id: version_id) = (case Inttab.lookup versions id of @@ -262,69 +266,72 @@ NONE => err_undef "command" id | SOME command => command); +end; -(* document execution *) - -fun discontinue_execution (State {execution = (_, _, running), ...}) = running := false; +fun remove_versions ids state = state |> map_state (fn (versions, _, execution) => + let + val _ = member (op =) ids (#1 execution) andalso + error ("Attempt to remove execution version " ^ print_id (#1 execution)); -fun cancel_execution (State {execution = (_, group, _), ...}) = Future.cancel_group group; -fun execution_tasks (State {execution = (_, group, _), ...}) = Future.group_tasks group; - -end; + val versions' = fold delete_version ids versions; + val commands' = + (versions', Inttab.empty) |-> + Inttab.fold (fn (_, version) => nodes_of version |> + Graph.fold (fn (_, (node, _)) => node |> + iterate_entries (fn ((_, id), _) => + SOME o Inttab.insert (K true) (id, the_command state id)))); + in (versions', commands', execution) end); -(** edit operations **) +(** document execution **) -(* execute *) +val discontinue_execution = execution_of #> (fn (_, _, running) => running := false); -local +val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group); -fun finished_theory node = - (case Exn.capture (Command.memo_result o the) (get_result node) of - Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st - | _ => false); +fun terminate_execution state = + let + val (_, group, _) = execution_of state; + val _ = Future.cancel_group group; + in Future.join_tasks (Future.group_tasks group) end; -in - -fun execute version_id state = - state |> map_state (fn (versions, commands, _) => - let - val version = the_version state version_id; +fun start_execution state = + let + fun finished_theory node = + (case Exn.capture (Command.memo_result o the) (get_result node) of + Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st + | _ => false); - fun run node command_id 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 group = Future.new_group NONE; - val running = Unsynchronized.ref true; + fun run node command_id 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 = ~2, interrupts = false} - (fn () => - iterate_entries (fn ((_, id), opt_exec) => fn () => - (case opt_exec of - SOME (_, exec) => if ! running then SOME (run node id exec) else NONE - | NONE => NONE)) node ())); - - in (versions, commands, (version_id, group, running)) end); - -end; + val (version_id, group, running) = execution_of state; + val _ = + nodes_of (the_version state version_id) |> 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 = ~2, interrupts = false} + (fn () => + iterate_entries (fn ((_, id), opt_exec) => fn () => + (case opt_exec of + SOME (_, exec) => if ! running then SOME (run node id exec) else NONE + | NONE => NONE)) node ())); + in () end; -(* update *) + +(** document update **) local @@ -446,7 +453,7 @@ val nodes = nodes_of new_version; val is_required = make_required nodes; - val _ = Future.join_tasks (execution_tasks state); + val _ = terminate_execution state; val updated = nodes |> Graph.schedule (fn deps => fn (name, node) => @@ -519,23 +526,6 @@ end; -(* remove versions *) - -fun remove_versions ids state = state |> map_state (fn (versions, _, execution) => - let - val _ = member (op =) ids (#1 execution) andalso - error ("Attempt to remove execution version " ^ print_id (#1 execution)); - - val versions' = fold delete_version ids versions; - val commands' = - (versions', Inttab.empty) |-> - Inttab.fold (fn (_, version) => nodes_of version |> - Graph.fold (fn (_, (node, _)) => node |> - iterate_entries (fn ((_, id), _) => - SOME o Inttab.insert (K true) (id, the_command state id)))); - in (versions', commands', execution) end); - - (** global state **) diff -r c0e8c98ee50e -r 0dbe6c69eda2 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Tue Apr 10 23:05:24 2012 +0200 +++ b/src/Pure/PIDE/protocol.ML Wed Apr 11 11:44:21 2012 +0200 @@ -50,15 +50,16 @@ fn (a, []) => Document.Perspective (map int_atom a)])) end; - val (assignment, state1) = Document.update old_id new_id edits state; + val (assignment, state') = Document.update old_id new_id edits state; val _ = Output.protocol_message Isabelle_Markup.assign_execs ((new_id, assignment) |> let open XML.Encode in pair int (list (pair int (option int))) end |> YXML.string_of_body); - val state2 = Document.execute new_id state1; - in state2 end)); + + val _ = Document.start_execution state'; + in state' end)); val _ = Isabelle_Process.protocol_command "Document.remove_versions"