# HG changeset patch
# User wenzelm
# Date 1535810934 -7200
# Node ID 5f44ad150ed8f1b895bcd391325898054bcd2bf4
# Parent  a8728e3f98220e8353dd29092a4415ca4204fdb1
more robust: memoize interrupt (e.g. resource problem) -- avoid multiple attempts;

diff -r a8728e3f9822 -r 5f44ad150ed8 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Sat Sep 01 14:25:03 2018 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Sat Sep 01 16:08:54 2018 +0200
@@ -16,7 +16,7 @@
   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_result: {strict: bool} -> 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
   val force_value: 'a lazy -> 'a lazy
   val map: ('a -> 'b) -> 'a lazy -> 'b lazy
@@ -80,8 +80,8 @@
 
 (* force result *)
 
-fun force_result (Value a) = Exn.Res a
-  | force_result (Lazy var) =
+fun force_result _ (Value a) = Exn.Res a
+  | force_result {strict} (Lazy var) =
       (case peek (Lazy var) of
         SOME res => res
       | NONE =>
@@ -104,19 +104,22 @@
                     val res0 = Exn.capture (restore_attributes e) ();
                     val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
                     val res = Future.join_result x;
-                    (*semantic race: some other threads might see the same
-                      interrupt, until there is a fresh start*)
                     val _ =
-                      if Exn.is_interrupt_exn res
-                      then Synchronized.change var (fn _ => Expr (name, e))
-                      else Synchronized.assign var (Result (Future.value_result res));
+                      if not (Exn.is_interrupt_exn res) then
+                        Synchronized.assign var (Result (Future.value_result res))
+                      else if strict then
+                        Synchronized.assign var
+                          (Result (Future.value_result (Exn.Exn (Fail "Interrupt"))))
+                      (*semantic race: some other threads might see the same
+                        interrupt, until there is a fresh start*)
+                      else Synchronized.change var (fn _ => Expr (name, e));
                   in res end
               | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
             end) ());
 
 end;
 
-fun force x = Exn.release (force_result x);
+fun force x = Exn.release (force_result {strict = false} x);
 
 fun force_value x = if is_value x then x else value (force x);
 
@@ -133,7 +136,8 @@
 fun consolidate xs =
   let
     val unfinished =
-      xs |> map_filter (fn x => if is_finished x then NONE else SOME (fn () => force_result x));
+      xs |> map_filter (fn x =>
+        if is_finished x then NONE else SOME (fn () => force_result {strict = false} x));
     val _ =
       if Future.relevant unfinished then
         ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} unfinished)
@@ -144,7 +148,7 @@
 (* future evaluation *)
 
 fun future params x =
-  if is_finished x then Future.value_result (force_result x)
+  if is_finished x then Future.value_result (force_result {strict = false} x)
   else (singleton o Future.forks) params (fn () => force x);
 
 
diff -r a8728e3f9822 -r 5f44ad150ed8 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sat Sep 01 14:25:03 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Sat Sep 01 16:08:54 2018 +0200
@@ -443,7 +443,7 @@
 fun run_process execution_id exec_id process =
   let val group = Future.worker_subgroup () in
     if Execution.running execution_id exec_id [group] then
-      ignore (task_context group Lazy.force_result process)
+      ignore (task_context group Lazy.force_result {strict = true} process)
     else ()
   end;