# HG changeset patch
# User wenzelm
# Date 1420978367 -3600
# Node ID 8a6788917b323fa09a428086f32d925e489cb159
# Parent  2183c731f0a7d2c14625cbcfac12cccd8bbc6f04
do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);

diff -r 2183c731f0a7 -r 8a6788917b32 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Sun Jan 11 12:46:19 2015 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Sun Jan 11 13:12:47 2015 +0100
@@ -14,7 +14,6 @@
   val peek: 'a lazy -> 'a Exn.result option
   val is_running: 'a lazy -> bool
   val is_finished: 'a lazy -> bool
-  val finished_result: 'a lazy -> 'a Exn.result option
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
   val map: ('a -> 'b) -> 'a lazy -> 'b lazy
@@ -55,15 +54,6 @@
   is_future (fn res =>
     Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))) x;
 
-fun finished_result (Lazy var) =
-  (case Synchronized.value var of
-    Expr _ => NONE
-  | Result res =>
-      if Future.is_finished res then
-        let val result = Future.join_result res
-        in if Exn.is_interrupt_exn result then NONE else SOME result end
-      else NONE);
-
 
 (* force result *)
 
diff -r 2183c731f0a7 -r 8a6788917b32 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Jan 11 12:46:19 2015 +0100
+++ b/src/Pure/PIDE/command.ML	Sun Jan 11 13:12:47 2015 +0100
@@ -143,11 +143,7 @@
 val eval_running = Execution.is_running_exec o eval_exec_id;
 fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process;
 
-fun eval_result (Eval {exec_id, eval_process}) =
-  (case Lazy.finished_result eval_process of
-    SOME result => Exn.release result
-  | NONE => error ("Unfinished execution result: " ^ Document_ID.print exec_id));
-
+fun eval_result (Eval {eval_process, ...}) = Lazy.force eval_process;
 val eval_result_state = #state o eval_result;
 
 local
diff -r 2183c731f0a7 -r 8a6788917b32 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Sun Jan 11 12:46:19 2015 +0100
+++ b/src/Pure/PIDE/execution.ML	Sun Jan 11 13:12:47 2015 +0100
@@ -66,14 +66,9 @@
 fun running execution_id exec_id groups =
   change_state_result (fn (execution_id', execs) =>
     let
-      val continue = execution_id = execution_id';
-      val execs' =
-        if continue then
-          Inttab.update_new (exec_id, (groups, [])) execs
-            handle Inttab.DUP dup =>
-              raise Fail ("Execution already registered: " ^ Document_ID.print dup)
-        else execs;
-    in (continue, (execution_id', execs')) end);
+      val ok = execution_id = execution_id' andalso not (Inttab.defined execs exec_id);
+      val execs' = execs |> ok ? Inttab.update (exec_id, (groups, []));
+    in (ok, (execution_id', execs')) end);
 
 fun peek exec_id =
   (case Inttab.lookup (#2 (get_state ())) exec_id of