Monadification of coqtop queries in CoqIDE

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16150 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 1 deletions

diff --git a/ide/coq.mli b/ide/coq.mli
index 230ff0b0b..a666c3cc2 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -49,7 +49,19 @@ type handle
 *)
 
 type void
-type 'a task = handle -> ('a -> void) -> void
+type 'a task
+
+val return : 'a -> 'a task
+(** Monadic return of values as tasks. *)
+
+val bind : 'a task -> ('a -> 'b task) -> 'b task
+(** Monadic binding of tasks *)
+
+val lift : (unit -> 'a) -> 'a task
+(** Return the impertative computation waiting to be processed. *)
+
+val seq : unit task -> 'a task -> 'a task
+(** Sequential composition *)
 
 (** Check if coqtop is computing, i.e. already has a current task *)
 val is_computing : coqtop -> bool