just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
authorwenzelm
Wed Apr 11 11:44:21 2012 +0200 (2012-04-11 ago)
changeset 474200dbe6c69eda2
parent 47419 c0e8c98ee50e
child 47421 9624408d8827
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
explicit terminate_execution;
tuned source structure;
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Apr 10 23:05:24 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Apr 11 11:44:21 2012 +0200
     1.3 @@ -25,12 +25,12 @@
     1.4    type state
     1.5    val init_state: state
     1.6    val define_command: command_id -> string -> string -> state -> state
     1.7 +  val remove_versions: version_id list -> state -> state
     1.8    val discontinue_execution: state -> unit
     1.9    val cancel_execution: state -> unit
    1.10 -  val execute: version_id -> state -> state
    1.11 +  val start_execution: state -> unit
    1.12    val update: version_id -> version_id -> edit list -> state ->
    1.13      (command_id * exec_id option) list * state
    1.14 -  val remove_versions: version_id list -> state -> state
    1.15    val state: unit -> state
    1.16    val change_state: (state -> state) -> unit
    1.17  end;
    1.18 @@ -144,7 +144,7 @@
    1.19      NONE => err_undef "command entry" id
    1.20    | SOME (exec, _) => exec);
    1.21  
    1.22 -fun the_default_entry node (SOME id) = (id, (the_default (no_id, no_exec) (the_entry node id)))
    1.23 +fun the_default_entry node (SOME id) = (id, the_default (no_id, no_exec) (the_entry node id))
    1.24    | the_default_entry _ NONE = (no_id, (no_id, no_exec));
    1.25  
    1.26  fun update_entry id exec =
    1.27 @@ -220,14 +220,18 @@
    1.28    make_state (Inttab.make [(no_id, empty_version)], Inttab.empty,
    1.29      (no_id, Future.new_group NONE, Unsynchronized.ref false));
    1.30  
    1.31 +fun execution_of (State {execution, ...}) = execution;
    1.32 +
    1.33  
    1.34  (* document versions *)
    1.35  
    1.36  fun define_version (id: version_id) version =
    1.37 -  map_state (fn (versions, commands, execution) =>
    1.38 -    let val versions' = Inttab.update_new (id, version) versions
    1.39 -      handle Inttab.DUP dup => err_dup "document version" dup
    1.40 -    in (versions', commands, execution) end);
    1.41 +  map_state (fn (versions, commands, _) =>
    1.42 +    let
    1.43 +      val versions' = Inttab.update_new (id, version) versions
    1.44 +        handle Inttab.DUP dup => err_dup "document version" dup;
    1.45 +      val execution' = (id, Future.new_group NONE, Unsynchronized.ref true);
    1.46 +    in (versions', commands, execution') end);
    1.47  
    1.48  fun the_version (State {versions, ...}) (id: version_id) =
    1.49    (case Inttab.lookup versions id of
    1.50 @@ -262,69 +266,72 @@
    1.51      NONE => err_undef "command" id
    1.52    | SOME command => command);
    1.53  
    1.54 +end;
    1.55  
    1.56 -(* document execution *)
    1.57 -
    1.58 -fun discontinue_execution (State {execution = (_, _, running), ...}) = running := false;
    1.59 +fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
    1.60 +  let
    1.61 +    val _ = member (op =) ids (#1 execution) andalso
    1.62 +      error ("Attempt to remove execution version " ^ print_id (#1 execution));
    1.63  
    1.64 -fun cancel_execution (State {execution = (_, group, _), ...}) = Future.cancel_group group;
    1.65 -fun execution_tasks (State {execution = (_, group, _), ...}) = Future.group_tasks group;
    1.66 -
    1.67 -end;
    1.68 +    val versions' = fold delete_version ids versions;
    1.69 +    val commands' =
    1.70 +      (versions', Inttab.empty) |->
    1.71 +        Inttab.fold (fn (_, version) => nodes_of version |>
    1.72 +          Graph.fold (fn (_, (node, _)) => node |>
    1.73 +            iterate_entries (fn ((_, id), _) =>
    1.74 +              SOME o Inttab.insert (K true) (id, the_command state id))));
    1.75 +  in (versions', commands', execution) end);
    1.76  
    1.77  
    1.78  
    1.79 -(** edit operations **)
    1.80 +(** document execution **)
    1.81  
    1.82 -(* execute *)
    1.83 +val discontinue_execution = execution_of #> (fn (_, _, running) => running := false);
    1.84  
    1.85 -local
    1.86 +val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group);
    1.87  
    1.88 -fun finished_theory node =
    1.89 -  (case Exn.capture (Command.memo_result o the) (get_result node) of
    1.90 -    Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st
    1.91 -  | _ => false);
    1.92 +fun terminate_execution state =
    1.93 +  let
    1.94 +    val (_, group, _) = execution_of state;
    1.95 +    val _ = Future.cancel_group group;
    1.96 +  in Future.join_tasks (Future.group_tasks group) end;
    1.97  
    1.98 -in
    1.99 -
   1.100 -fun execute version_id state =
   1.101 -  state |> map_state (fn (versions, commands, _) =>
   1.102 -    let
   1.103 -      val version = the_version state version_id;
   1.104 +fun start_execution state =
   1.105 +  let
   1.106 +    fun finished_theory node =
   1.107 +      (case Exn.capture (Command.memo_result o the) (get_result node) of
   1.108 +        Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st
   1.109 +      | _ => false);
   1.110  
   1.111 -      fun run node command_id exec =
   1.112 -        let
   1.113 -          val (_, print) = Command.memo_eval exec;
   1.114 -          val _ =
   1.115 -            if visible_command node command_id
   1.116 -            then ignore (Lazy.future Future.default_params print)
   1.117 -            else ();
   1.118 -        in () end;
   1.119 -
   1.120 -      val group = Future.new_group NONE;
   1.121 -      val running = Unsynchronized.ref true;
   1.122 +    fun run node command_id exec =
   1.123 +      let
   1.124 +        val (_, print) = Command.memo_eval exec;
   1.125 +        val _ =
   1.126 +          if visible_command node command_id
   1.127 +          then ignore (Lazy.future Future.default_params print)
   1.128 +          else ();
   1.129 +      in () end;
   1.130  
   1.131 -      val _ =
   1.132 -        nodes_of version |> Graph.schedule
   1.133 -          (fn deps => fn (name, node) =>
   1.134 -            if not (visible_node node) andalso finished_theory node then
   1.135 -              Future.value ()
   1.136 -            else
   1.137 -              (singleton o Future.forks)
   1.138 -                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
   1.139 -                  deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
   1.140 -                (fn () =>
   1.141 -                  iterate_entries (fn ((_, id), opt_exec) => fn () =>
   1.142 -                    (case opt_exec of
   1.143 -                      SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
   1.144 -                    | NONE => NONE)) node ()));
   1.145 -
   1.146 -    in (versions, commands, (version_id, group, running)) end);
   1.147 -
   1.148 -end;
   1.149 +    val (version_id, group, running) = execution_of state;
   1.150 +    val _ =
   1.151 +      nodes_of (the_version state version_id) |> Graph.schedule
   1.152 +        (fn deps => fn (name, node) =>
   1.153 +          if not (visible_node node) andalso finished_theory node then
   1.154 +            Future.value ()
   1.155 +          else
   1.156 +            (singleton o Future.forks)
   1.157 +              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
   1.158 +                deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
   1.159 +              (fn () =>
   1.160 +                iterate_entries (fn ((_, id), opt_exec) => fn () =>
   1.161 +                  (case opt_exec of
   1.162 +                    SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
   1.163 +                  | NONE => NONE)) node ()));
   1.164 +  in () end;
   1.165  
   1.166  
   1.167 -(* update *)
   1.168 +
   1.169 +(** document update **)
   1.170  
   1.171  local
   1.172  
   1.173 @@ -446,7 +453,7 @@
   1.174      val nodes = nodes_of new_version;
   1.175      val is_required = make_required nodes;
   1.176  
   1.177 -    val _ = Future.join_tasks (execution_tasks state);
   1.178 +    val _ = terminate_execution state;
   1.179      val updated =
   1.180        nodes |> Graph.schedule
   1.181          (fn deps => fn (name, node) =>
   1.182 @@ -519,23 +526,6 @@
   1.183  end;
   1.184  
   1.185  
   1.186 -(* remove versions *)
   1.187 -
   1.188 -fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
   1.189 -  let
   1.190 -    val _ = member (op =) ids (#1 execution) andalso
   1.191 -      error ("Attempt to remove execution version " ^ print_id (#1 execution));
   1.192 -
   1.193 -    val versions' = fold delete_version ids versions;
   1.194 -    val commands' =
   1.195 -      (versions', Inttab.empty) |->
   1.196 -        Inttab.fold (fn (_, version) => nodes_of version |>
   1.197 -          Graph.fold (fn (_, (node, _)) => node |>
   1.198 -            iterate_entries (fn ((_, id), _) =>
   1.199 -              SOME o Inttab.insert (K true) (id, the_command state id))));
   1.200 -  in (versions', commands', execution) end);
   1.201 -
   1.202 -
   1.203  
   1.204  (** global state **)
   1.205  
     2.1 --- a/src/Pure/PIDE/protocol.ML	Tue Apr 10 23:05:24 2012 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.ML	Wed Apr 11 11:44:21 2012 +0200
     2.3 @@ -50,15 +50,16 @@
     2.4                    fn (a, []) => Document.Perspective (map int_atom a)]))
     2.5              end;
     2.6  
     2.7 -        val (assignment, state1) = Document.update old_id new_id edits state;
     2.8 +        val (assignment, state') = Document.update old_id new_id edits state;
     2.9          val _ =
    2.10            Output.protocol_message Isabelle_Markup.assign_execs
    2.11              ((new_id, assignment) |>
    2.12                let open XML.Encode
    2.13                in pair int (list (pair int (option int))) end
    2.14                |> YXML.string_of_body);
    2.15 -        val state2 = Document.execute new_id state1;
    2.16 -      in state2 end));
    2.17 +
    2.18 +        val _ = Document.start_execution state';
    2.19 +      in state' end));
    2.20  
    2.21  val _ =
    2.22    Isabelle_Process.protocol_command "Document.remove_versions"