Plutôt que de faire "Load" silencieusement, en profiter pour traduire

le fichier chargé


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4410 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 6 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 28d2dc5d1..c8d69b26b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -104,18 +104,22 @@ let pr_comments = function
   | None -> mt()
   | Some l -> h 0 (List.fold_left (++) (mt ()) (List.rev l))
 
-let not_loading_file = ref true
-
 let rec vernac_com interpfun (loc,com) =
   let rec interp = function
     | VernacLoad (verbosely, fname) ->
         let ch = !chan_translate in
+        if Options.do_translate () then begin
+          let _,f = find_file_in_path (Library.get_load_path ())
+            (make_suffix fname ".v") in
+          chan_translate:=open_out (f^"8")
+        end;
         begin try
-          not_loading_file := false;
           read_vernac_file verbosely (make_suffix fname ".v");
-          not_loading_file := true
+          if Options.do_translate () then close_out !chan_translate;
+          chan_translate := ch
         with e ->
-	  not_loading_file := true;
+          if Options.do_translate () then close_out !chan_translate;
+          chan_translate := ch;
 	  raise e end;
 
     | VernacList l -> List.iter (fun (_,v) -> interp v) l
@@ -141,7 +145,7 @@ let rec vernac_com interpfun (loc,com) =
   in 
   try
     Options.v7_only := false;
-    if do_translate () & !not_loading_file then
+    if do_translate () then
       (Format.set_formatter_out_channel !chan_translate;
        Format.set_max_boxes max_int;
        (match com with