From f3a6d9080842899e50a44e9474ac0f9a475d5db1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Wed, 17 Dec 2014 14:51:29 +0100
Subject: 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.
---
 test-suite/ide/blocking-futures.fake | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 test-suite/ide/blocking-futures.fake

(limited to 'test-suite/ide')

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
-- 
cgit v1.2.3