Pour cacher le contenu de Load au traducteur

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

1 files changed, 9 insertions, 5 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 09df9611b5..28d2dc5d1c 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -104,15 +104,19 @@ 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
         begin try
-          chan_translate := stdout;
-          read_vernac_file verbosely (make_suffix fname ".v")
-        with _ -> () end;
-        chan_translate := ch
+          not_loading_file := false;
+          read_vernac_file verbosely (make_suffix fname ".v");
+          not_loading_file := true
+        with e ->
+	  not_loading_file := true;
+	  raise e end;
 
     | VernacList l -> List.iter (fun (_,v) -> interp v) l
 
@@ -137,7 +141,7 @@ let rec vernac_com interpfun (loc,com) =
   in 
   try
     Options.v7_only := false;
-    if do_translate () then
+    if do_translate () & !not_loading_file then
       (Format.set_formatter_out_channel !chan_translate;
        Format.set_max_boxes max_int;
        (match com with