From f3a6d9080842899e50a44e9474ac0f9a475d5db1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi 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. --- lib/future.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/future.ml') diff --git a/lib/future.ml b/lib/future.ml index 52a060c93..ff5d9ab52 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); -- cgit v1.2.3