Avoid Dumpglob dependency on Lexer

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

6 files changed, 37 insertions, 44 deletions

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 58577356b..9fde5e219 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -60,11 +60,6 @@ let previous_state = ref MultFiles
 let pause () = previous_state := !glob_output; glob_output := NoGlob
 let continue () = glob_output := !previous_state
 
-type coqdoc_state = Lexer.location_table
-
-let coqdoc_freeze = Lexer.location_table
-let coqdoc_unfreeze = Lexer.restore_location_table
-
 open Decl_kinds
 
 let type_of_logical_kind = function
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 16fa04ef9..469df1222 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -22,10 +22,6 @@ val dump_to_dotglob : unit -> unit
 val pause : unit -> unit
 val continue : unit -> unit
 
-type coqdoc_state = Lexer.location_table
-val coqdoc_freeze : unit -> coqdoc_state
-val coqdoc_unfreeze : coqdoc_state -> unit
-
 val add_glob : Pp.loc -> Globnames.global_reference -> unit
 val add_glob_kn : Pp.loc -> Names.kernel_name -> unit
 
diff --git a/interp/interp.mllib b/interp/interp.mllib
index ad3350f91..6d7e92111 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,5 +1,3 @@
-Tok
-Lexer
 Constrexpr_ops
 Notation_ops
 Topconstr
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 8414ec766..9adbb939a 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,3 +1,5 @@
+Tok
+Lexer
 Extend
 Extrawit
 Pcoq
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index cb14ff482..3936d2e80 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -109,11 +109,11 @@ let add_compile verbose s =
   compile_list := (verbose,s) :: !compile_list
 let compile_files () =
   let init_state = States.freeze() in
-  let coqdoc_init_state = Dumpglob.coqdoc_freeze () in
+  let coqdoc_init_state = Lexer.location_table () in
     List.iter
       (fun (v,f) ->
 	 States.unfreeze init_state;
-	 Dumpglob.coqdoc_unfreeze coqdoc_init_state;
+	 Lexer.restore_location_table coqdoc_init_state;
 	 if Flags.do_beautify () then
 	   with_option beautify_file (Vernac.compile v) f
 	 else
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 32387e793..3f3453b81 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -197,41 +197,43 @@ let pr_new_syntax loc ocom =
   States.unfreeze fs;
   Format.set_formatter_out_channel stdout
 
+let save_translator_coqdoc () =
+  (* translator state *)
+  let ch = !chan_beautify in
+  let cl = !Pp.comments in
+  let cs = Lexer.com_state() in
+  (* end translator state *)
+  let coqdocstate = Lexer.location_table () in
+  ch,cl,cs,coqdocstate
+
+let restore_translator_coqdoc (ch,cl,cs,coqdocstate) =
+  if !Flags.beautify_file then close_out !chan_beautify;
+  chan_beautify := ch;
+  Pp.comments := cl;
+  Lexer.restore_com_state cs;
+  Lexer.restore_location_table coqdocstate
+
 let rec vernac_com interpfun checknav (loc,com) =
   let rec interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
-        (* translator state *)
-        let ch = !chan_beautify in
-        let cs = Lexer.com_state() in
-        let cl = !Pp.comments in
-        (* end translator state *)
-        (* coqdoc state *)
-        let cds = Dumpglob.coqdoc_freeze() in
-          if !Flags.beautify_file then
-	    begin
-              let _,f = find_file_in_path ~warn:(Flags.is_verbose())
-		(Library.get_load_paths ())
-		(CUnix.make_suffix fname ".v") in
-		chan_beautify := open_out (f^beautify_suffix);
-		Pp.comments := []
-            end;
-          begin
-	    try
-	      read_vernac_file verbosely (CUnix.make_suffix fname ".v");
-              if !Flags.beautify_file then close_out !chan_beautify;
-              chan_beautify := ch;
-              Lexer.restore_com_state cs;
-              Pp.comments := cl;
-              Dumpglob.coqdoc_unfreeze cds
-	    with e ->
-	      if !Flags.beautify_file then close_out !chan_beautify;
-              chan_beautify := ch;
-              Lexer.restore_com_state cs;
-              Pp.comments := cl;
-              Dumpglob.coqdoc_unfreeze cds;
-	      raise e
-	  end
+	let st = save_translator_coqdoc () in
+	if !Flags.beautify_file then
+	  begin
+            let _,f = find_file_in_path ~warn:(Flags.is_verbose())
+	      (Library.get_load_paths ())
+	      (CUnix.make_suffix fname ".v") in
+	    chan_beautify := open_out (f^beautify_suffix);
+	    Pp.comments := []
+          end;
+	begin
+	  try
+	    read_vernac_file verbosely (CUnix.make_suffix fname ".v");
+	    restore_translator_coqdoc st
+	  with e ->
+	    restore_translator_coqdoc st;
+	    raise e
+	end
 
     | VernacList l -> List.iter (fun (_,v) -> interp v) l