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

2 files changed, 15 insertions, 4 deletions

diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 95bd57ce67..6424cb3d9c 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 f1a97a163e..b44e62eb91 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