summaryrefslogtreecommitdiff
path: root/toplevel/vernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r--toplevel/vernac.ml65
1 files changed, 44 insertions, 21 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 84e20f5e..ed20fc60 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -51,6 +51,8 @@ let real_error = function
| 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".
@@ -97,6 +99,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 +120,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))
@@ -166,7 +181,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
@@ -204,9 +219,13 @@ let rec vernac_com interpfun (loc,com) =
| VernacList l -> List.iter (fun (_,v) -> interp v) l
+ | v when !just_parsing -> ()
+
| VernacFail v ->
- if not !just_parsing then begin try
- interp v; raise HasNotFailed
+ 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
| HasNotFailed ->
errorlabstrm "Fail" (str "The command has not failed !")
@@ -219,22 +238,17 @@ let rec vernac_com interpfun (loc,com) =
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
@@ -243,6 +257,7 @@ let rec vernac_com interpfun (loc,com) =
with e -> restore_timeout psh; raise e
in
try
+ checknav loc com;
current_timeout := !default_timeout;
if do_beautify () then pr_new_syntax loc (Some com);
interp com
@@ -256,13 +271,17 @@ and read_vernac_file verbosely s =
if verbosely then Vernacentries.interp
else Flags.silently Vernacentries.interp
in
+ let checknav loc cmd =
+ if is_navigation_vernac cmd then
+ user_error loc "Navigation commands forbidden in files"
+ 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_com interpfun (parse_sentence input);
+ vernac_com interpfun checknav (parse_sentence input);
pp_flush ()
done
with e -> (* whatever the exception *)
@@ -273,15 +292,21 @@ and read_vernac_file verbosely s =
if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None
| _ -> raise_with_file fname e
+(** [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. *)
-(* eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit
- * execute one vernacular command. 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 eval_expr last =
- vernac_com Vernacentries.interp last;
- Lib.add_frozen_state();
- Lib.mark_end_of_command()
+let checknav loc ast =
+ if is_deep_navigation_vernac ast then
+ user_error loc "Navigation commands forbidden in nested commands"
+
+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 *)
@@ -317,5 +342,3 @@ let compile verbosely f =
if !Flags.xml_export then !xml_end_library ();
Dumpglob.end_dump_glob ();
Library.save_library_to ldir (long_f_dot_v ^ "o")
-
-