summaryrefslogtreecommitdiff
path: root/toplevel/vernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r--toplevel/vernac.ml180
1 files changed, 118 insertions, 62 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index de732618..ed8e215f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <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 *)
(************************************************************************)
-(* $Id: vernac.ml 15025 2012-03-09 14:27:07Z glondu $ *)
-
(* Parsing of vernacular. *)
open Pp
@@ -18,6 +16,7 @@ open System
open Vernacexpr
open Vernacinterp
open Ppvernac
+open Compat
(* The functions in this module may raise (unexplainable!) exceptions.
Use the module Coqtoplevel, which catches these exceptions
@@ -27,6 +26,30 @@ exception DuringCommandInterp of Util.loc * exn
exception HasNotFailed
+(* When doing Load on a file, two behaviors are possible:
+
+ - either the history stack is grown by only one command,
+ the "Load" itself. This is mandatory for command-counting
+ interfaces (CoqIDE).
+
+ - either each individual sub-commands in the file is added
+ to the history stack. This allows commands like Show Script
+ to work across the loaded file boundary (cf. bug #2820).
+
+ The best of the two could probably be combined someday,
+ in the meanwhile we use a flag. *)
+
+let atomic_load = ref true
+
+let _ =
+ Goptions.declare_bool_option
+ { Goptions.optsync = true;
+ Goptions.optdepr = false;
+ Goptions.optname = "atomic registration of commands in a Load";
+ Goptions.optkey = ["Atomic";"Load"];
+ Goptions.optread = (fun () -> !atomic_load);
+ Goptions.optwrite = ((:=) atomic_load) }
+
(* Specifies which file is read. The intermediate file names are
discarded here. The Drop exception becomes an error. We forget
if the error ocurred during interpretation or not *)
@@ -41,17 +64,19 @@ let raise_with_file file exc =
match re with
| Error_in_file (_, (b,f,loc), e) when loc <> dummy_loc ->
((b, f, loc), e)
- | Compat.Exc_located (loc, e) when loc <> dummy_loc ->
+ | Loc.Exc_located (loc, e) when loc <> dummy_loc ->
((false,file, loc), e)
- | Compat.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
+ | Loc.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
in
raise (Error_in_file (file, inner, disable_drop inex))
let real_error = function
- | Compat.Exc_located (_, e) -> e
+ | Loc.Exc_located (_, e) -> e
| Error_in_file (_, _, e) -> e
| e -> e
+let user_error loc s = Util.user_err_loc (loc,"_",str s)
+
(** Timeout handling *)
(** A global default timeout, controled by option "Set Default Timeout n".
@@ -62,6 +87,7 @@ let default_timeout = ref None
let _ =
Goptions.declare_int_option
{ Goptions.optsync = true;
+ Goptions.optdepr = false;
Goptions.optname = "the default timeout";
Goptions.optkey = ["Default";"Timeout"];
Goptions.optread = (fun () -> !default_timeout);
@@ -97,6 +123,18 @@ let restore_timeout = function
(* restore handler *)
Sys.set_signal Sys.sigalrm psh
+
+(* Open an utf-8 encoded file and skip the byte-order mark if any *)
+
+let open_utf8_file_in fname =
+ let is_bom s =
+ Char.code s.[0] = 0xEF && Char.code s.[1] = 0xBB && Char.code s.[2] = 0xBF
+ in
+ let in_chan = open_in fname in
+ let s = " " in
+ if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
+ in_chan
+
(* Opening and closing a channel. Open it twice when verbose: the first
channel is used to read the commands, and the second one to print them.
Note: we could use only one thanks to seek_in, but seeking on and on in
@@ -106,8 +144,9 @@ let open_file_twice_if verbosely fname =
let paths = Library.get_load_paths () in
let _,longfname =
find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
- let in_chan = open_in longfname in
- let verb_ch = if verbosely then Some (open_in longfname) else None in
+ let in_chan = open_utf8_file_in longfname in
+ let verb_ch =
+ if verbosely then Some (open_utf8_file_in longfname) else None in
let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
(in_chan, longfname, (po, verb_ch))
@@ -117,7 +156,7 @@ let close_input in_chan (_,verb) =
match verb with
| Some verb_ch -> close_in verb_ch
| _ -> ()
- with _ -> ()
+ with e when Errors.noncritical e -> ()
let verbose_phrase verbch loc =
let loc = unloc loc in
@@ -133,8 +172,8 @@ let verbose_phrase verbch loc =
exception End_of_input
-let parse_phrase (po, verbch) =
- match Pcoq.Gram.Entry.parse Pcoq.main_entry po with
+let parse_sentence (po, verbch) =
+ match Pcoq.Gram.entry_parse Pcoq.main_entry po with
| Some (loc,_ as com) -> verbose_phrase verbch loc; com
| None -> raise End_of_input
@@ -166,7 +205,7 @@ let pr_new_syntax loc ocom =
States.unfreeze fs;
Format.set_formatter_out_channel stdout
-let rec vernac_com interpfun (loc,com) =
+let rec vernac_com interpfun checknav (loc,com) =
let rec interp = function
| VernacLoad (verbosely, fname) ->
let fname = expand_path_macros fname in
@@ -193,98 +232,117 @@ let rec vernac_com interpfun (loc,com) =
Lexer.restore_com_state cs;
Pp.comments := cl;
Dumpglob.coqdoc_unfreeze cds
- with e ->
+ with reraise ->
if !Flags.beautify_file then close_out !chan_beautify;
chan_beautify := ch;
Lexer.restore_com_state cs;
Pp.comments := cl;
Dumpglob.coqdoc_unfreeze cds;
- raise e
+ raise reraise
end
| VernacList l -> List.iter (fun (_,v) -> interp v) l
+ | v when !just_parsing -> ()
+
| VernacFail v ->
- if not !just_parsing then begin try
+ begin try
(* If the command actually works, ignore its effects on the state *)
States.with_state_protection
(fun v -> interp v; raise HasNotFailed) v
- with e -> match real_error e with
+ with e when Errors.noncritical e -> match real_error e with
| HasNotFailed ->
errorlabstrm "Fail" (str "The command has not failed !")
| e ->
- (* if [e] is an anomaly, the next function will re-raise it *)
- let msg = Cerrors.explain_exn_no_anomaly e in
- if_verbose msgnl (str "The command has indeed failed with message:" ++
- fnl () ++ str "=> " ++ hov 0 msg)
+ (* Anomalies are re-raised by the next line *)
+ let msg = Errors.print_no_anomaly e in
+ if_verbose msgnl
+ (str "The command has indeed failed with message:" ++
+ fnl () ++ str "=> " ++ hov 0 msg)
end
| VernacTime v ->
- if not !just_parsing then begin
let tstart = System.get_time() in
interp v;
let tend = System.get_time() in
msgnl (str"Finished transaction in " ++
System.fmt_time_difference tstart tend)
- end
| VernacTimeout(n,v) ->
- if not !just_parsing then begin
current_timeout := Some n;
interp v
- end
| v ->
- if not !just_parsing then
let psh = default_set_timeout () in
try
States.with_heavy_rollback interpfun
Cerrors.process_vernac_interp_error v;
restore_timeout psh
- with e -> restore_timeout psh; raise e
+ with reraise -> restore_timeout psh; raise reraise
in
try
+ checknav loc com;
current_timeout := !default_timeout;
if do_beautify () then pr_new_syntax loc (Some com);
interp com
- with e ->
+ with any ->
Format.set_formatter_out_channel stdout;
- raise (DuringCommandInterp (loc, e))
-
-and vernac interpfun input =
- vernac_com interpfun (parse_phrase input)
+ raise (DuringCommandInterp (loc, any))
and read_vernac_file verbosely s =
Flags.make_warn verbosely;
let interpfun =
- if verbosely then
- Vernacentries.interp
+ if verbosely then Vernacentries.interp
+ else Flags.silently Vernacentries.interp
+ in
+ let checknav loc cmd =
+ if is_navigation_vernac cmd && not (is_reset cmd) then
+ user_error loc "Navigation commands forbidden in files"
+ in
+ let end_inner_command cmd =
+ if !atomic_load || is_reset cmd then
+ Lib.mark_end_of_command () (* for Reset in coqc or coqtop -l *)
else
- Flags.silently Vernacentries.interp
+ Backtrack.mark_command cmd; (* for Show Script, cf bug #2820 *)
in
- let (in_chan, fname, input) = open_file_twice_if verbosely s in
+ let (in_chan, fname, input) =
+ open_file_twice_if verbosely s in
try
(* we go out of the following infinite loop when a End_of_input is
* raised, which means that we raised the end of the file being loaded *)
- while true do vernac interpfun input; pp_flush () done
- with e -> (* whatever the exception *)
+ while true do
+ let loc_ast = parse_sentence input in
+ vernac_com interpfun checknav loc_ast;
+ end_inner_command (snd loc_ast);
+ pp_flush ()
+ done
+ with reraise -> (* whatever the exception *)
Format.set_formatter_out_channel stdout;
close_input in_chan input; (* we must close the file first *)
- match real_error e with
+ match real_error reraise with
| End_of_input ->
if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None
- | _ -> raise_with_file fname e
+ | _ -> raise_with_file fname reraise
+
+(** [eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit]
+ It 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. *)
-(* raw_do_vernac : char Stream.t -> unit
- * parses and executes one command of the vernacular char stream.
- * Marks the end of the command in the lib_stk with a new label to
- * make vernac undoing easier. Also freeze state to speed up
- * backtracking. *)
+let checknav loc ast =
+ if is_deep_navigation_vernac ast then
+ user_error loc "Navigation commands forbidden in nested commands"
-let raw_do_vernac po =
- vernac Vernacentries.interp (po,None);
- Lib.add_frozen_state();
- Lib.mark_end_of_command()
+let eval_expr ?(preserving=false) loc_ast =
+ vernac_com Vernacentries.interp checknav loc_ast;
+ if not preserving && not (is_navigation_vernac (snd loc_ast)) then
+ Backtrack.mark_command (snd loc_ast)
+
+(* raw_do_vernac : Pcoq.Gram.parsable -> unit
+ * vernac_step . parse_sentence *)
+let raw_do_vernac po = eval_expr (parse_sentence (po,None))
(* XML output hooks *)
let xml_start_library = ref (fun _ -> ())
@@ -298,24 +356,22 @@ let load_vernac verb file =
chan_beautify :=
if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
try
+ Lib.mark_end_of_command (); (* in case we're still in coqtop init *)
read_vernac_file verb file;
if !Flags.beautify_file then close_out !chan_beautify;
- with e ->
+ with reraise ->
if !Flags.beautify_file then close_out !chan_beautify;
- raise_with_file file e
+ raise_with_file file reraise
(* Compile a vernac file (f is assumed without .v suffix) *)
let compile verbosely f =
let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
- if Dumpglob.multi_dump () then
- Dumpglob.open_glob_file (f ^ ".glob");
- Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
- if !Flags.xml_export then !xml_start_library ();
- let _ = load_vernac verbosely long_f_dot_v in
- if Pfedit.get_all_proof_names () <> [] then
- (message "Error: There are pending proofs"; exit 1);
- if !Flags.xml_export then !xml_end_library ();
- if Dumpglob.multi_dump () then Dumpglob.close_glob_file ();
- Library.save_library_to ldir (long_f_dot_v ^ "o")
-
-
+ Dumpglob.start_dump_glob long_f_dot_v;
+ Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
+ if !Flags.xml_export then !xml_start_library ();
+ let _ = load_vernac verbosely long_f_dot_v in
+ if Pfedit.get_all_proof_names () <> [] then
+ (message "Error: There are pending proofs"; exit 1);
+ if !Flags.xml_export then !xml_end_library ();
+ Dumpglob.end_dump_glob ();
+ Library.save_library_to ldir (long_f_dot_v ^ "o")
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 08:13:08 +0000