Réinitialisation de token_number à chaque compilation d'un nouveau fichier (fixe le bug #914)

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

2 files changed, 34 insertions, 29 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index cb0d89143..94a70ccda 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -108,14 +108,16 @@ let add_compile verbose s =
   compile_list := (verbose,s) :: !compile_list
 let compile_files () =
   let init_state = States.freeze() in
-  List.iter
-    (fun (v,f) ->
-      States.unfreeze init_state;
-      if Options.do_translate () then
-	with_option translate_file (Vernac.compile v) f
-      else
-	Vernac.compile v f)
-    (List.rev !compile_list)
+  let coqdoc_init_state = Constrintern.coqdoc_freeze () in
+    List.iter
+      (fun (v,f) ->
+	 States.unfreeze init_state;
+	 Constrintern.coqdoc_unfreeze coqdoc_init_state;
+	 if Options.do_translate () then
+	   with_option translate_file (Vernac.compile v) f
+	 else
+	   Vernac.compile v f)
+      (List.rev !compile_list)
 
 let re_exec_version = ref ""
 let set_byte () = re_exec_version := "byte"
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index d44227a80..f3bc0793f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -126,27 +126,30 @@ let rec vernac_com interpfun (loc,com) =
         (* end translator state *)
         (* coqdoc state *)
         let cds = Constrintern.coqdoc_freeze() in
-        if !Options.translate_file then begin
-          let _,f = find_file_in_path (Library.get_load_paths ())
-            (make_suffix fname ".v") in
-          chan_translate := open_out (f^"8");
-          Pp.comments := []
-        end;
-        begin try
-          read_vernac_file verbosely (make_suffix fname ".v");
-          if !Options.translate_file then close_out !chan_translate;
-          chan_translate := ch;
-          Lexer.restore_com_state cs;
-          Pp.comments := cl;
-          Constrintern.coqdoc_unfreeze cds;
-        with e ->
-          if !Options.translate_file then close_out !chan_translate;
-          chan_translate := ch;
-          Lexer.restore_com_state cs;
-          Pp.comments := cl;
-          Constrintern.coqdoc_unfreeze cds;
-          raise e end;
-
+          if !Options.translate_file then 
+	    begin
+              let _,f = find_file_in_path (Library.get_load_paths ())
+		(make_suffix fname ".v") in
+		chan_translate := open_out (f^"8");
+		Pp.comments := []
+            end;
+          begin 
+	    try
+	      read_vernac_file verbosely (make_suffix fname ".v");
+              if !Options.translate_file then close_out !chan_translate;
+              chan_translate := ch;
+              Lexer.restore_com_state cs;
+              Pp.comments := cl;
+              Constrintern.coqdoc_unfreeze cds
+	    with e -> 
+	      if !Options.translate_file then close_out !chan_translate;
+              chan_translate := ch;
+              Lexer.restore_com_state cs;
+              Pp.comments := cl;
+              Constrintern.coqdoc_unfreeze cds;
+	      raise e
+	  end
+	      
     | VernacList l -> List.iter (fun (_,v) -> interp v) l
 
     | VernacTime v ->