diff options
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 29 |
1 files changed, 16 insertions, 13 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index 8a1fa3ed..40a6dea8 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Coq : Interaction with the Coq toplevel *) @@ -115,15 +117,11 @@ val try_grab : coqtop -> unit task -> (unit -> unit) -> unit type 'a query = 'a Interface.value task (** A type abbreviation for coqtop specific answers *) -val add : ?logger:Ideutils.logger -> - Interface.add_sty -> Interface.add_rty query +val add : Interface.add_sty -> Interface.add_rty query val edit_at : Interface.edit_at_sty -> Interface.edit_at_rty query -val query : ?logger:Ideutils.logger -> - Interface.query_sty -> Interface.query_rty query -val status : ?logger:Ideutils.logger -> - Interface.status_sty -> Interface.status_rty query -val goals : ?logger:Ideutils.logger -> - Interface.goals_sty -> Interface.goals_rty query +val query : Interface.query_sty -> Interface.query_rty query +val status : Interface.status_sty -> Interface.status_rty query +val goals : Interface.goals_sty -> Interface.goals_rty query val evars : Interface.evars_sty -> Interface.evars_rty query val hints : Interface.hints_sty -> Interface.hints_rty query val mkcases : Interface.mkcases_sty -> Interface.mkcases_rty query @@ -143,7 +141,8 @@ sig val bool_items : bool_descr list val set : t -> bool -> unit - val set_printing_width : int -> unit + + val printing_unfocused: unit -> bool (** [enforce] transmits to coq the current option values. It is also called by [goals] and [evars] above. *) @@ -173,3 +172,7 @@ val check_connection : string list -> unit may terminate coqide in case of trouble *) val interrupter : (int -> unit) ref +val save_all : (unit -> unit) ref + +(* Flags to be used for ideslave *) +val ideslave_coqtop_flags : string option ref |