src/Pure/PIDE/execution.ML
changeset 52775 e0169f13bd37
parent 52760 8517172b9626
child 52784 4ba2e8b9972f
     1.1 --- a/src/Pure/PIDE/execution.ML	Mon Jul 29 16:52:04 2013 +0200
     1.2 +++ b/src/Pure/PIDE/execution.ML	Mon Jul 29 18:59:58 2013 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4    val discontinue: unit -> unit
     1.5    val is_running: Document_ID.execution -> bool
     1.6    val running: Document_ID.execution -> Document_ID.exec -> bool
     1.7 -  val finished: Document_ID.exec -> unit
     1.8    val cancel: Document_ID.exec -> unit
     1.9    val terminate: Document_ID.exec -> unit
    1.10  end;
    1.11 @@ -52,12 +51,6 @@
    1.12            else execs;
    1.13        in SOME (continue, (execution_id', execs')) end);
    1.14  
    1.15 -fun finished exec_id =
    1.16 -  Synchronized.change state
    1.17 -    (apsnd (fn execs =>
    1.18 -      Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
    1.19 -        error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
    1.20 -
    1.21  fun peek_list exec_id =
    1.22    the_list (Inttab.lookup (snd (Synchronized.value state)) exec_id);
    1.23