diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /toplevel/coqloop.mli | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'toplevel/coqloop.mli')
-rw-r--r-- | toplevel/coqloop.mli | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli new file mode 100644 index 00000000..8ed661e6 --- /dev/null +++ b/toplevel/coqloop.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp + +(** The Coq toplevel loop. *) + +(** 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 len : int; (** number of chars in the buffer *) + mutable bols : int list; (** offsets in str of begining of lines *) + mutable tokens : Pcoq.Gram.parsable; (** stream of tokens *) + mutable start : int } (** stream count of the first char of the buffer *) + +(** The input buffer of stdin. *) + +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 + +(** Parse and execute one vernac command. *) + +val do_vernac : unit -> unit + +(** Main entry point of Coq: read and execute vernac commands. *) + +val loop : unit -> unit |