diff options
Diffstat (limited to 'toplevel/coqloop.mli')
| -rw-r--r-- | toplevel/coqloop.mli | 17 |
1 files changed, 6 insertions, 11 deletions
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index bbb9b138..b11f13d3 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -10,9 +10,6 @@ (** 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. *) @@ -21,7 +18,7 @@ type input_buffer = { 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 *) + mutable tokens : Pcoq.Parsable.t; (** stream of tokens *) mutable start : int } (** stream count of the first char of the buffer *) (** The input buffer of stdin. *) @@ -30,13 +27,11 @@ val top_buffer : input_buffer val set_prompt : (unit -> string) -> unit (** Toplevel feedback printer. *) -val coqloop_feed : Feedback.feedback -> unit - -(** Parse and execute one vernac command. *) -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 coqloop_feed : Topfmt.execution_phase -> Feedback.feedback -> unit (** Last document seen after `Drop` *) val drop_last_doc : Vernac.State.t option ref +val drop_args : Coqargs.coq_cmdopts option ref + +(** Main entry point of Coq: read and execute vernac commands. *) +val loop : opts:Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit |