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/vernac.mli | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'toplevel/vernac.mli')
-rw-r--r-- | toplevel/vernac.mli | 26 |
1 files changed, 11 insertions, 15 deletions
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index c1ac2154..affc2171 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <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 *) @@ -12,28 +12,16 @@ Raises [End_of_file] if EOF (or Ctrl-D) is reached. *) val parse_sentence : Pcoq.Gram.parsable * in_channel option -> - Util.loc * Vernacexpr.vernac_expr + Loc.t * Vernacexpr.vernac_expr (** Reads and executes vernac commands from a stream. The boolean [just_parsing] disables interpretation of commands. *) -exception DuringCommandInterp of Util.loc * exn exception End_of_input val just_parsing : bool ref -(** [eval_expr] executes one vernacular command. By default the command is - considered as non-state-preserving, in which case we add it to the - Backtrack stack (triggering a save of a frozen state and the generation - of a new state label). An example of state-preserving command is one coming - from the query panel of Coqide. *) - -val eval_expr : ?preserving:bool -> Util.loc * Vernacexpr.vernac_expr -> unit -val raw_do_vernac : Pcoq.Gram.parsable -> unit - -(** Set XML hooks *) -val set_xml_start_library : (unit -> unit) -> unit -val set_xml_end_library : (unit -> unit) -> unit +val eval_expr : Loc.t * Vernacexpr.vernac_expr -> unit (** Load a vernac file, verbosely or not. Errors are annotated with file and location *) @@ -44,3 +32,11 @@ val load_vernac : bool -> string -> unit (** Compile a vernac file, verbosely or not (f is assumed without .v suffix) *) val compile : bool -> string -> unit + +val is_navigation_vernac : Vernacexpr.vernac_expr -> bool + +(** Has an exception been annotated with some file locations ? *) + +type location_files = { outer : string; inner : string } + +val get_exn_files : Exninfo.info -> location_files option |