diff options
| -rw-r--r-- | ide/coq.ml | 6 | ||||
| -rw-r--r-- | ide/coq.mli | 30 | ||||
| -rw-r--r-- | ide/coqOps.ml | 19 | ||||
| -rw-r--r-- | ide/coqOps.mli | 19 |
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 : |