--- a/src/Pure/PIDE/execution.ML Mon Jul 29 16:52:04 2013 +0200
+++ b/src/Pure/PIDE/execution.ML Mon Jul 29 18:59:58 2013 +0200
@@ -11,7 +11,6 @@
val discontinue: unit -> unit
val is_running: Document_ID.execution -> bool
val running: Document_ID.execution -> Document_ID.exec -> bool
- val finished: Document_ID.exec -> unit
val cancel: Document_ID.exec -> unit
val terminate: Document_ID.exec -> unit
end;
@@ -52,12 +51,6 @@
else execs;
in SOME (continue, (execution_id', execs')) end);
-fun finished exec_id =
- Synchronized.change state
- (apsnd (fn execs =>
- Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
- error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
-
fun peek_list exec_id =
the_list (Inttab.lookup (snd (Synchronized.value state)) exec_id);