Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

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")
-
-