src/Pure/PIDE/exec.ML
changeset 52596 40298d383463
child 52602 00170ef1dc39
equal deleted inserted replaced
52595:76883c1e1c53 52596:40298d383463
       
     1 (*  Title:      Pure/PIDE/exec.ML
       
     2     Author:     Makarius
       
     3 
       
     4 Global management of command execution fragments.
       
     5 *)
       
     6 
       
     7 signature EXEC =
       
     8 sig
       
     9   val is_stable: Document_ID.exec -> bool
       
    10   val running: Document_ID.exec -> unit
       
    11   val finished: Document_ID.exec -> unit
       
    12   val canceled: Document_ID.exec -> unit
       
    13   val purge_unstable: unit -> unit
       
    14 end;
       
    15 
       
    16 structure Exec: EXEC =
       
    17 struct
       
    18 
       
    19 val running_execs =
       
    20   Synchronized.var "Exec.running_execs" (Inttab.empty: {stable: bool} Inttab.table);
       
    21 
       
    22 fun is_stable exec_id =
       
    23   not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
       
    24   (case Inttab.lookup (Synchronized.value running_execs) exec_id of
       
    25     NONE => true
       
    26   | SOME {stable} => stable);
       
    27 
       
    28 fun running exec_id =
       
    29   Synchronized.change running_execs (Inttab.update_new (exec_id, {stable = true}));
       
    30 
       
    31 fun finished exec_id =
       
    32   Synchronized.change running_execs (Inttab.delete exec_id);
       
    33 
       
    34 fun canceled exec_id =
       
    35   Synchronized.change running_execs (Inttab.update (exec_id, {stable = false}));
       
    36 
       
    37 fun purge_unstable () =
       
    38   Synchronized.guarded_access running_execs
       
    39     (fn tab =>
       
    40       let
       
    41         val unstable = Inttab.fold (fn (exec_id, {stable = false}) => cons exec_id | _ => I) tab [];
       
    42         val tab' = fold Inttab.delete unstable tab;
       
    43       in SOME ((), tab') end);
       
    44 
       
    45 end;
       
    46