do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);
authorwenzelm
Sun Jan 11 13:12:47 2015 +0100 (2015-01-11 ago)
changeset 593488a6788917b32
parent 59347 2183c731f0a7
child 59349 3bde948f439c
do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);
src/Pure/Concurrent/lazy.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/execution.ML
     1.1 --- a/src/Pure/Concurrent/lazy.ML	Sun Jan 11 12:46:19 2015 +0100
     1.2 +++ b/src/Pure/Concurrent/lazy.ML	Sun Jan 11 13:12:47 2015 +0100
     1.3 @@ -14,7 +14,6 @@
     1.4    val peek: 'a lazy -> 'a Exn.result option
     1.5    val is_running: 'a lazy -> bool
     1.6    val is_finished: 'a lazy -> bool
     1.7 -  val finished_result: 'a lazy -> 'a Exn.result option
     1.8    val force_result: 'a lazy -> 'a Exn.result
     1.9    val force: 'a lazy -> 'a
    1.10    val map: ('a -> 'b) -> 'a lazy -> 'b lazy
    1.11 @@ -55,15 +54,6 @@
    1.12    is_future (fn res =>
    1.13      Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))) x;
    1.14  
    1.15 -fun finished_result (Lazy var) =
    1.16 -  (case Synchronized.value var of
    1.17 -    Expr _ => NONE
    1.18 -  | Result res =>
    1.19 -      if Future.is_finished res then
    1.20 -        let val result = Future.join_result res
    1.21 -        in if Exn.is_interrupt_exn result then NONE else SOME result end
    1.22 -      else NONE);
    1.23 -
    1.24  
    1.25  (* force result *)
    1.26  
     2.1 --- a/src/Pure/PIDE/command.ML	Sun Jan 11 12:46:19 2015 +0100
     2.2 +++ b/src/Pure/PIDE/command.ML	Sun Jan 11 13:12:47 2015 +0100
     2.3 @@ -143,11 +143,7 @@
     2.4  val eval_running = Execution.is_running_exec o eval_exec_id;
     2.5  fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process;
     2.6  
     2.7 -fun eval_result (Eval {exec_id, eval_process}) =
     2.8 -  (case Lazy.finished_result eval_process of
     2.9 -    SOME result => Exn.release result
    2.10 -  | NONE => error ("Unfinished execution result: " ^ Document_ID.print exec_id));
    2.11 -
    2.12 +fun eval_result (Eval {eval_process, ...}) = Lazy.force eval_process;
    2.13  val eval_result_state = #state o eval_result;
    2.14  
    2.15  local
     3.1 --- a/src/Pure/PIDE/execution.ML	Sun Jan 11 12:46:19 2015 +0100
     3.2 +++ b/src/Pure/PIDE/execution.ML	Sun Jan 11 13:12:47 2015 +0100
     3.3 @@ -66,14 +66,9 @@
     3.4  fun running execution_id exec_id groups =
     3.5    change_state_result (fn (execution_id', execs) =>
     3.6      let
     3.7 -      val continue = execution_id = execution_id';
     3.8 -      val execs' =
     3.9 -        if continue then
    3.10 -          Inttab.update_new (exec_id, (groups, [])) execs
    3.11 -            handle Inttab.DUP dup =>
    3.12 -              raise Fail ("Execution already registered: " ^ Document_ID.print dup)
    3.13 -        else execs;
    3.14 -    in (continue, (execution_id', execs')) end);
    3.15 +      val ok = execution_id = execution_id' andalso not (Inttab.defined execs exec_id);
    3.16 +      val execs' = execs |> ok ? Inttab.update (exec_id, (groups, []));
    3.17 +    in (ok, (execution_id', execs')) end);
    3.18  
    3.19  fun peek exec_id =
    3.20    (case Inttab.lookup (#2 (get_state ())) exec_id of