src/Pure/PIDE/document.ML
changeset 41634 28d94383249c
parent 41630 a7a93df23664
child 41672 2f70b1ddd09f
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Jan 25 22:59:03 2011 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Jan 27 12:24:00 2011 +0100
     1.3 @@ -18,6 +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 define_command: command_id -> string -> state -> state
     1.9    val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
    1.10    val execute: version_id -> state -> state
    1.11 @@ -181,6 +182,15 @@
    1.12      NONE => err_undef "command execution" id
    1.13    | SOME exec => exec);
    1.14  
    1.15 +
    1.16 +(* document execution *)
    1.17 +
    1.18 +fun cancel (State {execution, ...}) =
    1.19 +  List.app Future.cancel execution;
    1.20 +
    1.21 +fun await_cancellation (State {execution, ...}) =
    1.22 +  ignore (Future.join_results execution);
    1.23 +
    1.24  end;
    1.25  
    1.26  
    1.27 @@ -324,20 +334,19 @@
    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 _ = List.app Future.cancel execution;
    1.32 -      fun await_cancellation () = Future.join_results execution;
    1.33 +      val _ = cancel state;
    1.34  
    1.35        val execution' = (* FIXME proper node deps *)
    1.36          [Future.fork_pri 1 (fn () =>
    1.37            let
    1.38 -            val _ = await_cancellation ();
    1.39 +            val _ = await_cancellation state;
    1.40              val _ =
    1.41                node_names_of version |> List.app (fn name =>
    1.42                  fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
    1.43                      (get_node version name) ());
    1.44            in () end)];
    1.45  
    1.46 -      val _ = await_cancellation ();
    1.47 +      val _ = await_cancellation state;  (* FIXME async!? *)
    1.48  
    1.49      in (versions, commands, execs, execution') end);
    1.50