diff options
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 |