Protection table des locations lors de Load (pour coqdoc)

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

3 files changed, 18 insertions, 4 deletions

diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 95bd57ce6..6424cb3d9 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -487,8 +487,10 @@ let loct_add loct i loc =
   end;
   !loct.(i) <- Some loc
 
-let current_location_function =
-  ref (fun _ -> failwith "No location function is set")
+let current_location_table = ref (ref [||])
+
+let location_function n =
+  loct_func !current_location_table n
 
 let func cs =
   let loct = loct_create () in
@@ -498,9 +500,13 @@ let func cs =
          let (tok, loc) = next_token cs in
 	 loct_add loct i loc; Some tok)
   in
-  current_location_function := loct_func loct;
+  current_location_table := loct;
   (ts, loct_func loct)
 
+type location_table = (int * int) option array ref
+let location_table () = !current_location_table
+let restore_location_table t = current_location_table := t
+
 (* Names of tokens, for this lexer, used in Grammar error messages *)
 
 let token_text = function
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index f1a97a163..b44e62eb9 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -23,7 +23,12 @@ val add_keyword : string -> unit
 val is_keyword : string -> bool
 
 val func : char Stream.t -> (string * string) Stream.t * (int -> int * int)
-val current_location_function : (int -> int  * int) ref
+val location_function : int -> int  * int
+
+(* for coqdoc *)
+type location_table
+val location_table : unit -> location_table
+val restore_location_table : location_table -> unit
 
 val check_ident : string -> unit
 val check_special_token : string -> unit
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f5410a8a1..1119d59c2 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -170,6 +170,7 @@ let rec vernac_com interpfun (loc,com) =
     | VernacLoad (verbosely, fname) ->
         let ch = !chan_translate in
         let cs = Lexer.com_state() in
+        let lt = Lexer.location_table() in
         let cl = !Pp.comments in
         if !Options.translate_file then begin
           let _,f = find_file_in_path (Library.get_load_path ())
@@ -182,11 +183,13 @@ let rec vernac_com interpfun (loc,com) =
           if !Options.translate_file then close_out !chan_translate;
           chan_translate := ch;
           Lexer.restore_com_state cs;
+          Lexer.restore_location_table lt;
           Pp.comments := cl
         with e ->
           if !Options.translate_file then close_out !chan_translate;
           chan_translate := ch;
           Lexer.restore_com_state cs;
+          Lexer.restore_location_table lt;
           Pp.comments := cl;
           raise e end;