# HG changeset patch
# User wenzelm
# Date 1535804703 -7200
# Node ID a8728e3f98220e8353dd29092a4415ca4204fdb1
# Parent  d4681a748873c6a40df4f68d023a11253ac9ac84
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);

diff -r d4681a748873 -r a8728e3f9822 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Sat Sep 01 13:38:44 2018 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Sat Sep 01 14:25:03 2018 +0200
@@ -15,6 +15,7 @@
   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
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
   val force_value: 'a lazy -> 'a lazy
@@ -59,12 +60,22 @@
         Expr _ => false
       | Result res => not (Future.is_finished res));
 
+fun is_finished_future res =
+  Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res));
+
 fun is_finished (Value _) = true
   | is_finished (Lazy var) =
       (case Synchronized.value var of
         Expr _ => false
-      | Result res =>
-          Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res)));
+      | Result res => is_finished_future res);
+
+fun finished_result (Value a) = Exn.Res a
+  | finished_result (Lazy var) =
+      let fun fail () = Exn.Exn (Fail "Unfinished lazy") in
+        (case Synchronized.value var of
+          Expr _ => fail ()
+        | Result res => if is_finished_future res then Future.join_result res else fail ())
+      end;
 
 
 (* force result *)
diff -r d4681a748873 -r a8728e3f9822 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sat Sep 01 13:38:44 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Sat Sep 01 14:25:03 2018 +0200
@@ -180,7 +180,7 @@
 fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process;
 
 fun eval_result (Eval {eval_process, ...}) =
-  task_context (Future.worker_subgroup ()) Lazy.force eval_process;
+  Exn.release (Lazy.finished_result eval_process);
 
 val eval_result_command = #command o eval_result;
 val eval_result_state = #state o eval_result;