Removing export of location_table outside of cLexer.

It was not used any more by coqdoc since b8194b22 (Dec 2010).

The table is now only part of the lexer function closure
(and only in the camlp5 case).

4 files changed, 7 insertions, 30 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 181c4b7fd8..0090117f67 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -626,12 +626,6 @@ let loct_func loct i =
 
 let loct_add loct i loc = Hashtbl.add loct i loc
 
-let current_location_table = ref (loct_create ())
-
-type location_table = (int, Compat.CompatLoc.t) Hashtbl.t
-let location_table () = !current_location_table
-let restore_location_table t = current_location_table := t
-
 (** {6 The lexer of Coq} *)
 
 (** Note: removing a token.
@@ -669,7 +663,6 @@ let func cs =
 	 cur_loc := Compat.after loc;
          loct_add loct i loc; Some tok)
   in
-  current_location_table := loct;
   (ts, loct_func loct)
 
 let lexer = {
@@ -706,7 +699,6 @@ end
 let mk () =
   let loct = loct_create () in
   let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in
-  current_location_table := loct; 
   let rec self init_loc (* FIXME *) =
     parser i
        [< (tok, loc) = next_token !cur_loc; s >] ->
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 3ad49eb74a..71edda760c 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -10,14 +10,6 @@ val add_keyword : string -> unit
 val remove_keyword : string -> unit
 val is_keyword : string -> bool
 
-(* val location_function : int -> Loc.t *)
-
-(** for coqdoc *)
-type location_table
-val location_table : unit -> location_table
-val restore_location_table : location_table -> unit
-
-
 (** [get_current_file fname] returns the filename used in locations emitted by
     the lexer *)
 val get_current_file : unit -> string
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7a67e0951f..26ef68262b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -228,11 +228,9 @@ let compile_files () =
   if !compile_list == [] then ()
   else
     let init_state = States.freeze ~marshallable:`No in
-    let coqdoc_init_state = CLexer.location_table () in
     Feedback.(add_feeder debug_feeder);
     List.iter (fun vf ->
         States.unfreeze init_state;
-        CLexer.restore_location_table coqdoc_init_state;
         compile_file vf)
       (List.rev !compile_list)
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b8e44db9a7..661a597aea 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -145,17 +145,12 @@ let pr_new_syntax (po,_) loc ocom =
   (* Reinstall the context of parsing which includes the bindings of comments to locations *)
   Pcoq.Gram.with_parsable po (pr_new_syntax_in_context loc) ocom
 
-let save_translator_coqdoc () =
-  (* translator state *)
-  let ch = !chan_beautify in
-  (* end translator state *)
-  let coqdocstate = CLexer.location_table () in
-  ch,coqdocstate
+let save_translator () =
+  !chan_beautify
 
-let restore_translator_coqdoc (ch,coqdocstate) =
+let restore_translator ch =
   if !Flags.beautify_file then close_out !chan_beautify;
-  chan_beautify := ch;
-  CLexer.restore_location_table coqdocstate
+  chan_beautify := ch
 
 (* For coqtop -time, we display the position in the file,
    and a glimpse of the executed command *)
@@ -191,7 +186,7 @@ let rec vernac_com input checknav (loc,com) =
 	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
         let fname = CUnix.make_suffix fname ".v" in
         let f = Loadpath.locate_file fname in
-	let st = save_translator_coqdoc () in
+	let st = save_translator () in
         let old_lexer_file = CLexer.get_current_file () in
         CLexer.set_current_file f;
 	if !Flags.beautify_file then
@@ -201,11 +196,11 @@ let rec vernac_com input checknav (loc,com) =
 	begin
 	  try
             Flags.silently (read_vernac_file verbosely) f;
-	    restore_translator_coqdoc st;
+	    restore_translator st;
             CLexer.set_current_file old_lexer_file;
 	  with reraise ->
             let reraise = CErrors.push reraise in
-	    restore_translator_coqdoc st;
+	    restore_translator st;
             CLexer.set_current_file old_lexer_file;
 	    iraise reraise
 	end