diff options
-rw-r--r-- | .depend | 19 | ||||
-rw-r--r-- | Makefile | 3 | ||||
-rw-r--r-- | toplevel/toplevel.ml | 14 | ||||
-rw-r--r-- | toplevel/toplevel.mli | 2 | ||||
-rw-r--r-- | toplevel/vernac.mli | 6 |
5 files changed, 26 insertions, 18 deletions
@@ -45,6 +45,7 @@ parsing/coqast.cmi: lib/dyn.cmi parsing/g_minicoq.cmi: kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ kernel/term.cmi parsing/pcoq.cmi: parsing/coqast.cmi +proofs/pfedit.cmi: lib/pp.cmi proofs/proof_trees.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ @@ -153,8 +154,12 @@ kernel/typing.cmx: kernel/constant.cmx kernel/environ.cmx kernel/generic.cmx \ kernel/typing.cmi kernel/univ.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi kernel/univ.cmi kernel/univ.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx kernel/univ.cmi +lib/bstack.cmo: lib/util.cmi lib/bstack.cmi +lib/bstack.cmx: lib/util.cmx lib/bstack.cmi lib/dyn.cmo: lib/util.cmi lib/dyn.cmi lib/dyn.cmx: lib/util.cmx lib/dyn.cmi +lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi +lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi lib/hashcons.cmo: lib/hashcons.cmi lib/hashcons.cmx: lib/hashcons.cmi lib/options.cmo: lib/options.cmi @@ -259,12 +264,14 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmx \ lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmx \ toplevel/protectedtoplevel.cmx lib/util.cmx toplevel/vernac.cmx \ toplevel/vernacinterp.cmi toplevel/toplevel.cmi -toplevel/vernac.cmo: parsing/ast.cmi library/discharge.cmi \ - library/library.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \ - lib/system.cmi toplevel/vernacinterp.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/ast.cmx library/discharge.cmi \ - library/library.cmx parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmx \ - lib/system.cmx toplevel/vernacinterp.cmi toplevel/vernac.cmi +toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ + library/library.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \ + lib/pp.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ + library/library.cmx lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmi \ + lib/pp.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmi \ + toplevel/vernac.cmi parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ toplevel/vernac.cmi parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi \ @@ -32,7 +32,8 @@ CAMLP4OBJS=gramlib.cma CONFIG=config/coq_config.cmo LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \ - lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo + lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \ + lib/bstack.cmo lib/edit.cmo KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \ kernel/sign.cmo kernel/evd.cmo kernel/constant.cmo \ diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index dcad19bed..643433e0c 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -40,8 +40,8 @@ let resynch_buffer ibuf = ibuf.start <- ibuf.start + ll | _ -> () -(* Read a char in an input channel, displaying a prompt af every - begining of line. *) +(* Read a char in an input channel, displaying a prompt at every + beginning of line. *) let prompt_char ic ibuf count = let bol = match ibuf.bols with @@ -125,8 +125,7 @@ let print_highlight_location ib (bp,ep) = let print_location_in_file s fname (bp,ep) = let errstrm = [< 'sTR"Error while reading "; 'sTR s; 'sTR" :"; 'fNL; 'sTR"File "; 'sTR ("\""^fname^"\"") >] in - if (bp,ep) = Ast.dummy_loc - then + if (bp,ep) = Ast.dummy_loc then [< errstrm; 'sTR", unknown location."; 'fNL >] else let ic = open_in fname in @@ -241,8 +240,8 @@ let rec discard_to_dot () = (* If the error occured while parsing, we read the input until a dot token - * in encountered. - *) + * in encountered. *) + let process_error = function | DuringCommandInterp _ as e -> e | e -> @@ -266,7 +265,8 @@ let do_vernac () = begin try raw_do_vernac top_buffer.tokens - with e -> mSGNL (print_toplevel_error (process_error e)) + with e -> + mSGNL (print_toplevel_error (process_error e)) end; flush_all() diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli index 3d04fc625..22caa2a9f 100644 --- a/toplevel/toplevel.mli +++ b/toplevel/toplevel.mli @@ -25,7 +25,7 @@ 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, + 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 diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 401598781..0c65b8693 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -3,18 +3,18 @@ (* Parsing of vernacular. *) -(* Like Exc_located, but specifies the outermost file read, the input buffer +(* Like [Exc_located], but specifies the outermost file read, the input buffer associated to the location of the error, and the error itself. *) exception Error_in_file of string * (string * Coqast.loc) * exn (* Read a vernac command on the specified input (parse only). - Raises End_of_file if EOF (or Ctrl-D) is reached. *) + Raises [End_of_file] if EOF (or Ctrl-D) is reached. *) val parse_phrase : Pcoq.Gram.parsable * in_channel option -> Coqast.t (* Reads and executes vernac commands from a stream. - The boolean just_parsing disables interpretation of commands. *) + The boolean [just_parsing] disables interpretation of commands. *) exception DuringCommandInterp of Coqast.loc * exn exception End_of_input |