diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2013-12-16 17:08:46 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2013-12-16 17:24:55 +0100 |
commit | 4759f60b04a278ecd46c8a120340ba55b185c6d1 (patch) | |
tree | f5e24b08d23bd5efc9d0f80b86cde32ad548220f /toplevel/coqloop.mli | |
parent | 9f005304183ca9c46f6516c08c3c0cc2f1efc05f (diff) |
A few fixes to the build system (mostly for ocamlbuild)
* vars.mli was mentionning Term instead of Constr, leading to a dep cycle
* Having a file named toplevel/toplevel.ml isn't a good idea when we also
have a toplevel/toplevel.mllib that ought to produce a toplevel.cma.
We rename toplevel.ml into Coqloop.ml
* Extra cleanup of toplevel.mllib :
- Ppextra isn't anywhere around (?!)
- Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway
- Vernacexpr is a .mli and shouldn't appear in an .mllib
* During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml)
* A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread
for coqchk).
Diffstat (limited to 'toplevel/coqloop.mli')
-rw-r--r-- | toplevel/coqloop.mli | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli new file mode 100644 index 000000000..1375f3361 --- /dev/null +++ b/toplevel/coqloop.mli @@ -0,0 +1,42 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Pcoq + +(** 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 : exn -> 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 |