Future: blocking by default

This makes queries like Print or Extraction block and not
raise the error "the value is not ready".  This should make
CoqIDE work for every kind of script.

2 files changed, 17 insertions, 1 deletions

diff --git a/lib/future.ml b/lib/future.ml
index 52a060c93a..ff5d9ab529 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -94,7 +94,7 @@ let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ())))
 
 let fix_exn_of ck = let _, fix_exn, _ = get ck in fix_exn
 
-let create_delegate ?(blocking=false) fix_exn =
+let create_delegate ?(blocking=true) fix_exn =
   let assignement signal ck = fun v ->
     let _, fix_exn, c = get ck in
     assert (match !c with Delegated _ -> true | _ -> false);
diff --git a/test-suite/ide/blocking-futures.fake b/test-suite/ide/blocking-futures.fake
new file mode 100644
index 0000000000..b63f09bcfc
--- /dev/null
+++ b/test-suite/ide/blocking-futures.fake
@@ -0,0 +1,16 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Extraction will force the future computation, assert it is blocking
+# Example courtesy of Jonathan (jonikelee)
+#
+ADD { Require Import List. }
+ADD { Import ListNotations. }
+ADD { Definition myrev{A}(l : list A) : {rl : list A | rl = rev l}. }
+ADD { Proof. }
+ADD {   induction l. }
+ADD {    eexists; reflexivity. }
+ADD {    cbn; destruct IHl as [rl' H]; rewrite <-H; eexists; reflexivity. }
+ADD { Qed. }
+ADD { Extraction myrev. }
+GOALS