src/Pure/PIDE/execution.ML
changeset 53375 78693e46a237
parent 53193 2ddc5e788f7c
child 54646 2b38549374ba
     1.1 --- a/src/Pure/PIDE/execution.ML	Tue Sep 03 01:12:40 2013 +0200
     1.2 +++ b/src/Pure/PIDE/execution.ML	Tue Sep 03 11:29:01 2013 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    val discontinue: unit -> unit
     1.5    val is_running: Document_ID.execution -> bool
     1.6    val is_running_exec: Document_ID.exec -> bool
     1.7 -  val running: Document_ID.execution -> Document_ID.exec -> bool
     1.8 +  val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool
     1.9    val peek: Document_ID.exec -> Future.group list
    1.10    val cancel: Document_ID.exec -> unit
    1.11    val terminate: Document_ID.exec -> unit
    1.12 @@ -33,7 +33,7 @@
    1.13  fun make_state (execution, execs) = State {execution = execution, execs = execs};
    1.14  fun map_state f (State {execution, execs}) = make_state (f (execution, execs));
    1.15  
    1.16 -val init_state = make_state (Document_ID.none, Inttab.empty);
    1.17 +val init_state = make_state (Document_ID.none, Inttab.make [(Document_ID.none, [])]);
    1.18  val state = Synchronized.var "Execution.state" init_state;
    1.19  
    1.20  fun get_state () = let val State args = Synchronized.value state in args end;
    1.21 @@ -58,18 +58,18 @@
    1.22  fun is_running_exec exec_id =
    1.23    Inttab.defined (#execs (get_state ())) exec_id;
    1.24  
    1.25 -fun running execution_id exec_id =
    1.26 -  Synchronized.guarded_access state
    1.27 +fun running execution_id exec_id groups =
    1.28 +  Synchronized.change_result state
    1.29      (fn State {execution = execution_id', execs} =>
    1.30        let
    1.31          val continue = execution_id = execution_id';
    1.32          val execs' =
    1.33            if continue then
    1.34 -            Inttab.update_new (exec_id, [Future.the_worker_group ()]) execs
    1.35 +            Inttab.update_new (exec_id, groups) execs
    1.36                handle Inttab.DUP dup =>
    1.37 -                error ("Execution already registered: " ^ Document_ID.print dup)
    1.38 +                raise Fail ("Execution already registered: " ^ Document_ID.print dup)
    1.39            else execs;
    1.40 -      in SOME (continue, make_state (execution_id', execs')) end);
    1.41 +      in (continue, make_state (execution_id', execs')) end);
    1.42  
    1.43  fun peek exec_id =
    1.44    Inttab.lookup_list (#execs (get_state ())) exec_id;
    1.45 @@ -89,7 +89,10 @@
    1.46      let
    1.47        val exec_id = the_default 0 (Position.parse_id pos);
    1.48        val group = Future.worker_subgroup ();
    1.49 -      val _ = change_state (apsnd (Inttab.cons_list (exec_id, group)));
    1.50 +      val _ = change_state (apsnd (fn execs =>
    1.51 +        if Inttab.defined execs exec_id
    1.52 +        then Inttab.cons_list (exec_id, group) execs
    1.53 +        else raise Fail ("Cannot fork from unregistered execution: " ^ Document_ID.print exec_id)));
    1.54  
    1.55        val future =
    1.56          (singleton o Future.forks)
    1.57 @@ -127,7 +130,7 @@
    1.58            if Inttab.defined execs' exec_id then ()
    1.59            else groups |> List.app (fn group =>
    1.60              if Task_Queue.is_canceled group then ()
    1.61 -            else error ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
    1.62 +            else raise Fail ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
    1.63      in execs' end);
    1.64  
    1.65  fun reset () =