src/Pure/PIDE/document.ML
changeset 49906 06a3570b0f0a
parent 49173 fa01a202399c
child 50201 c26369c9eda6
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Oct 18 09:19:37 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Oct 18 12:00:27 2012 +0200
     1.3 @@ -318,14 +318,8 @@
     1.4  (** document execution **)
     1.5  
     1.6  val discontinue_execution = execution_of #> (fn (_, _, running) => running := false);
     1.7 -
     1.8  val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group);
     1.9 -
    1.10 -fun terminate_execution state =
    1.11 -  let
    1.12 -    val (_, group, _) = execution_of state;
    1.13 -    val _ = Future.cancel_group group;
    1.14 -  in Future.join_tasks (Future.group_tasks group) end;
    1.15 +val terminate_execution = execution_of #> (fn (_, group, _) => Future.terminate group);
    1.16  
    1.17  fun start_execution state =
    1.18    let