Uniformization of Coq tasks

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

4 files changed, 38 insertions, 36 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index f165d2013..9baf3c782 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -266,7 +266,7 @@ type handle = {
 
 type status = New | Ready | Busy | Closed
 
-type task = handle -> (unit -> void) -> void
+type 'a task = handle -> ('a -> void) -> void
 
 type reset_kind = Planned | Unexpected
 
@@ -274,7 +274,7 @@ type coqtop = {
   (* non quoted command-line arguments of coqtop *)
   sup_args : string list;
   (* called whenever coqtop dies *)
-  mutable reset_handler : reset_kind -> task;
+  mutable reset_handler : reset_kind -> unit task;
   (* actual coqtop process and its status *)
   mutable handle : handle;
   mutable status : status;
@@ -494,7 +494,7 @@ let init_coqtop coqtop task =
 
 (** Cf [Ide_intf] for more details *)
 
-type 'a atask = handle -> ('a Interface.value -> void) -> void
+type 'a query = 'a Interface.value task
 
 let eval_call ?(logger=default_logger) call handle k =
   (** Send messages to coqtop and prepare the decoding of the answer *)
diff --git a/ide/coq.mli b/ide/coq.mli
index 52f58caa6..230ff0b0b 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -49,7 +49,7 @@ type handle
 *)
 
 type void
-type task = handle -> (unit->void) -> void
+type 'a task = handle -> ('a -> void) -> void
 
 (** Check if coqtop is computing, i.e. already has a current task *)
 val is_computing : coqtop -> bool
@@ -61,11 +61,11 @@ val spawn_coqtop : string list -> coqtop
 
 (** Register a handler called when a coqtop dies (badly or on purpose) *)
 type reset_kind = Planned | Unexpected
-val set_reset_handler : coqtop -> (reset_kind -> task) -> unit
+val set_reset_handler : coqtop -> (reset_kind -> unit task) -> unit
 
 (** Finish initializing a freshly spawned coqtop, by running a first task on it.
     The task should run its inner continuation at the end. *)
-val init_coqtop : coqtop -> task -> unit
+val init_coqtop : coqtop -> unit task -> unit
 
 (** Interrupt the current computation of coqtop. *)
 val break_coqtop : coqtop -> unit
@@ -100,7 +100,7 @@ val final_countdown : unit -> unit
       before its completion.
     - The task callback should run its inner continuation at the end. *)
 
-val try_grab : coqtop -> task -> (unit -> unit) -> unit
+val try_grab : coqtop -> unit task -> (unit -> unit) -> unit
 
 (** * Atomic calls to coqtop
 
@@ -111,18 +111,18 @@ val try_grab : coqtop -> task -> (unit -> unit) -> unit
   when this answer is available.
   Except for interp, we use the default logger for any call. *)
 
-type 'a atask = handle -> ('a Interface.value -> void) -> void
+type 'a query = 'a Interface.value task
 
 val interp : ?logger:Ideutils.logger -> ?raw:bool -> ?verbose:bool ->
-  string -> string atask
-val rewind : int -> int atask
-val status : Interface.status atask
-val goals : Interface.goals option atask
-val evars : Interface.evar list option atask
-val hints : (Interface.hint list * Interface.hint) option atask
-val inloadpath : string -> bool atask
-val mkcases : string -> string list list atask
-val search : Interface.search_flags -> string Interface.coq_object list atask
+  string -> string query
+val rewind : int -> int query
+val status : Interface.status query
+val goals : Interface.goals option query
+val evars : Interface.evar list option query
+val hints : (Interface.hint list * Interface.hint) option query
+val inloadpath : string -> bool query
+val mkcases : string -> string list list query
+val search : Interface.search_flags -> string Interface.coq_object list query
 
 (** A specialized version of [raw_interp] dedicated to set/unset options. *)
 
@@ -140,5 +140,5 @@ sig
   (** [enforce] transmits to coq the current option values.
       It is also called by [goals] and [evars] above. *)
 
-  val enforce : task
+  val enforce : unit task
 end
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 94036e9a1..c41db3e2d 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Coq
 open Ideutils
 
 type flag = [ `COMMENT | `UNSAFE ]
@@ -20,15 +21,15 @@ let prefs = Preferences.current
 
 class type ops =
 object
-  method go_to_insert : Coq.task
-  method tactic_wizard : string list -> Coq.task
-  method process_next_phrase : Coq.task
-  method process_until_end_or_error : Coq.task
-  method handle_reset_initial : Coq.reset_kind -> Coq.task
-  method raw_coq_query : string -> Coq.task
-  method show_goals : Coq.task
-  method backtrack_last_phrase : Coq.task
-  method initialize : Coq.task
+  method go_to_insert : unit task
+  method tactic_wizard : string list -> unit task
+  method process_next_phrase : unit task
+  method process_until_end_or_error : unit task
+  method handle_reset_initial : Coq.reset_kind -> unit task
+  method raw_coq_query : string -> unit task
+  method show_goals : unit task
+  method backtrack_last_phrase : unit task
+  method initialize : unit task
 end
 
 class coqops
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index acc80cd62..7e47ca23f 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -6,18 +6,19 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Coq
 
 class type ops =
 object
-  method go_to_insert : Coq.task
-  method tactic_wizard : string list -> Coq.task
-  method process_next_phrase : Coq.task
-  method process_until_end_or_error : Coq.task
-  method handle_reset_initial : Coq.reset_kind -> Coq.task
-  method raw_coq_query : string -> Coq.task
-  method show_goals : Coq.task
-  method backtrack_last_phrase : Coq.task
-  method initialize : Coq.task
+  method go_to_insert : unit task
+  method tactic_wizard : string list -> unit task
+  method process_next_phrase : unit task
+  method process_until_end_or_error : unit task
+  method handle_reset_initial : Coq.reset_kind -> unit task
+  method raw_coq_query : string -> unit task
+  method show_goals : unit task
+  method backtrack_last_phrase : unit task
+  method initialize : unit task
 end
 
 class coqops :