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  

     2.1 --- a/src/Pure/PIDE/isar_document.ML	Tue Jul 05 11:16:37 2011 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.ML	Tue Jul 05 11:45:48 2011 +0200
     2.3 @@ -30,8 +30,9 @@
     2.4                      (XML_Data.dest_option XML_Data.dest_int)
     2.5                      (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
     2.6  
     2.7 -      val _ = Document.cancel state;
     2.8 +      val await_cancellation = Document.cancel_execution state;
     2.9        val (updates, state') = Document.edit old_id new_id edits state;
    2.10 +      val _ = await_cancellation ();
    2.11        val _ =
    2.12          Output.status (Markup.markup (Markup.assign new_id)
    2.13            (implode (map (Markup.markup_only o Markup.edit) updates)));