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.

1 files changed, 16 insertions, 0 deletions

diff --git a/test-suite/ide/blocking-futures.fake b/test-suite/ide/blocking-futures.fake
new file mode 100644
index 000000000..b63f09bcf
--- /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