diff options
Diffstat (limited to 'toplevel/coqloop.mli')
| -rw-r--r-- | toplevel/coqloop.mli | 33 |
1 files changed, 17 insertions, 16 deletions
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index e40353e0..bbb9b138 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -1,21 +1,24 @@ (************************************************************************) -(* 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) *) (************************************************************************) -open Pp - (** The Coq toplevel loop. *) +(** -emacs option: printing includes emacs tags. *) +val print_emacs : bool ref + (** A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) type input_buffer = { - mutable prompt : unit -> string; - mutable str : string; (** buffer of already read characters *) + mutable prompt : Stm.doc -> string; + mutable str : Bytes.t; (** buffer of already read characters *) mutable len : int; (** number of chars in the buffer *) mutable bols : int list; (** offsets in str of begining of lines *) mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *) @@ -26,16 +29,14 @@ type input_buffer = { val top_buffer : input_buffer val set_prompt : (unit -> string) -> unit -(** Toplevel error explanation, dealing with locations, Drop, Ctrl-D - May raise only the following exceptions: [Drop] and [End_of_input], - meaning we get out of the Coq loop. *) - -val print_toplevel_error : Exninfo.iexn -> std_ppcmds +(** Toplevel feedback printer. *) +val coqloop_feed : Feedback.feedback -> unit (** Parse and execute one vernac command. *) - -val do_vernac : unit -> unit +val do_vernac : time:bool -> state:Vernac.State.t -> Vernac.State.t (** Main entry point of Coq: read and execute vernac commands. *) +val loop : time:bool -> state:Vernac.State.t -> Vernac.State.t -val loop : unit -> unit +(** Last document seen after `Drop` *) +val drop_last_doc : Vernac.State.t option ref |