Suppression de l'option -dump-glob et ajout d'une option -no-glob

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

3 files changed, 20 insertions, 10 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0c9b12bb4a..02044b2cf2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -113,6 +113,10 @@ let compile_files () =
       (fun (v,f) ->
 	 States.unfreeze init_state;
 	 Constrintern.coqdoc_unfreeze coqdoc_init_state;
+	 if !Flags.noglob then
+	   Flags.dump := false
+	 else
+	   Flags.dump_into_file (f^".glob");
 	 if Flags.do_translate () then
 	   with_option translate_file (Vernac.compile v) f
 	 else
@@ -231,8 +235,8 @@ let parse_args is_ide =
     | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem
     | "-load-vernac-object" :: []       -> usage ()
 
-    | "-dump-glob" :: f :: rem -> dump_into_file f; parse rem
-    | "-dump-glob" :: []       -> usage ()
+    | "-dump-glob" :: _ :: rem -> warning "option -dumpglob is obsolete"; parse rem
+    | ("-no-glob" | "-noglob") :: rem -> Flags.noglob := true; parse rem
 
     | "-require" :: f :: rem -> add_require f; parse rem
     | "-require" :: []       -> usage ()
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 4944bfede7..e00f7808ba 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -53,7 +53,7 @@ let print_usage_channel co command =
   -batch                 batch mode (exits just after arguments parsing)
   -boot                  boot mode (implies -q and -batch)
   -emacs                 tells Coq it is executed under Emacs
-  -dump-glob f           dump globalizations in file f (to be used by coqdoc)
+  -no-glob f             do not dump globalizations
   -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)
   -impredicative-set     set sort Set impredicative
   -dont-load-proofs      don't load opaque proofs in memory
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index ac834b2a58..c0ec552280 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -226,11 +226,17 @@ let load_vernac verb file =
 (* Compile a vernac file (f is assumed without .v suffix) *)
 let compile verbosely f =
   let ldir,long_f_dot_v = Library.start_library f in
-  if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
-  if !Flags.xml_export then !xml_start_library ();
-  let _ = load_vernac verbosely long_f_dot_v in
-  if Pfedit.get_all_proof_names () <> [] then
-    (message "Error: There are pending proofs"; exit 1);
-  if !Flags.xml_export then !xml_end_library ();
-  Library.save_library_to ldir (long_f_dot_v ^ "o")
+  let dumpstate = !Flags.dump in
+    if not !Flags.noglob then
+      (Flags.dump_into_file (f ^ ".glob");
+       Flags.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"));
+    if !Flags.xml_export then !xml_start_library ();
+    let _ = load_vernac verbosely long_f_dot_v in
+     if Pfedit.get_all_proof_names () <> [] then
+	(message "Error: There are pending proofs"; exit 1);
+      if !Flags.xml_export then !xml_end_library ();
+      if !Flags.dump then Flags.dump_it ();
+      Flags.dump := dumpstate;
+      Library.save_library_to ldir (long_f_dot_v ^ "o")
+