1.1 --- a/src/Pure/PIDE/document.ML Tue Jul 05 11:16:37 2011 +0200
1.2 +++ b/src/Pure/PIDE/document.ML Tue Jul 05 11:45:48 2011 +0200
1.3 @@ -18,7 +18,7 @@
1.4 type edit = string * ((command_id option * command_id option) list) option
1.5 type state
1.6 val init_state: state
1.7 - val cancel: state -> unit
1.8 + val cancel_execution: state -> unit -> unit
1.9 val define_command: command_id -> string -> state -> state
1.10 val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
1.11 val execute: version_id -> state -> state
1.12 @@ -185,11 +185,9 @@
1.13
1.14 (* document execution *)
1.15
1.16 -fun cancel (State {execution, ...}) =
1.17 - List.app Future.cancel execution;
1.18 -
1.19 -fun await_cancellation (State {execution, ...}) =
1.20 - ignore (Future.join_results execution);
1.21 +fun cancel_execution (State {execution, ...}) =
1.22 + (List.app Future.cancel execution;
1.23 + fn () => ignore (Future.join_results execution));
1.24
1.25 end;
1.26
1.27 @@ -338,20 +336,12 @@
1.28 fun force_exec NONE = ()
1.29 | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
1.30
1.31 - val _ = cancel state;
1.32 -
1.33 val execution' = (* FIXME proper node deps *)
1.34 Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
1.35 [fn () =>
1.36 - let
1.37 - val _ = await_cancellation state;
1.38 - val _ =
1.39 - node_names_of version |> List.app (fn name =>
1.40 - fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
1.41 - (get_node version name) ());
1.42 - in () end];
1.43 -
1.44 - val _ = await_cancellation state; (* FIXME async!? *)
1.45 + node_names_of version |> List.app (fn name =>
1.46 + fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
1.47 + (get_node version name) ())];
1.48
1.49 in (versions, commands, execs, execution') end);
1.50