diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-17 14:51:29 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-17 15:05:05 +0100 |
commit | f3a6d9080842899e50a44e9474ac0f9a475d5db1 (patch) | |
tree | 92c11419d7545eb4488b861e888102d990262b3d /lib/future.ml | |
parent | df32bf741e872195cc0630088871ccc5bad0906d (diff) |
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.
Diffstat (limited to 'lib/future.ml')
-rw-r--r-- | lib/future.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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); |