Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from de coqdoc (compatibilité)

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

4 files changed, 38 insertions, 35 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7e92b804ca..1a856d477d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -240,8 +240,12 @@ let parse_args is_ide =
     | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem
     | "-load-vernac-object" :: []       -> usage ()
 
-    | "-dump-glob" :: _ :: rem -> warning "option -dumpglob is obsolete"; parse rem
-    | ("-no-glob" | "-noglob") :: rem -> Flags.noglob := true; parse rem
+    | "-dump-glob" :: "stdout" :: rem -> Dumpglob.dump_to_stdout (); parse rem
+	  (* À ne pas documenter : l'option 'stdout' n'étant
+	     éventuellement utile que pour le debugging... *)
+    | "-dump-glob" :: f :: rem -> Dumpglob.dump_into_file f; parse rem
+    | "-dump-glob" :: []       -> usage ()
+    | ("-no-glob" | "-noglob") :: rem -> Dumpglob.noglob (); parse rem
 
     | "-require" :: f :: rem -> add_require f; parse rem
     | "-require" :: []       -> usage ()
@@ -265,7 +269,7 @@ let parse_args is_ide =
     | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
     | "-emacs-U" :: rem -> Flags.print_emacs := true; 
 	Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem
-	
+	    
     | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem
 
     | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 124ce0593e..417a496f8a 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -57,7 +57,8 @@ 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
-  -no-glob f             do not dump globalizations
+  -noglob f              do not dump globalizations
+  -dump-glob f           dump globalizations in file f (to be used by coqdoc)
   -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 d3c556147d..ae35b0fa1a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -226,18 +226,16 @@ 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
-  let dumpstate = !Flags.dump in
-    if not !Flags.noglob then
-      (Flags.dump := true; 
-       Dumpglob.open_glob_file f;
-       Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"));
+    if Dumpglob.multi_dump () then 
+      Dumpglob.open_glob_file (f ^ ".glob");
+    if Dumpglob.dump () then
+      Dumpglob.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 Dumpglob.close_glob_file ();
-      Flags.dump := dumpstate;
+      if Dumpglob.multi_dump () then Dumpglob.close_glob_file ();
       Library.save_library_to ldir (long_f_dot_v ^ "o")
 
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 246e35dadd..65b36edb60 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -277,7 +277,7 @@ let print_located_module r =
 
 let global_with_alias r =
   let gr = global_with_alias r in
-    if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr;
+    if Dumpglob.dump () then Dumpglob.add_glob (loc_of_reference r) gr;
     gr
 
 (**********)
@@ -308,7 +308,7 @@ let start_proof_and_print k l hook =
   if !pcoq <> None then (Option.get !pcoq).start_proof ()
 
 let vernac_definition (local,_,_ as k) (loc,id as lid) def hook =
-  if !Flags.dump then Dumpglob.dump_definition lid false "def";
+  if Dumpglob.dump () then Dumpglob.dump_definition lid false "def";
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
  	if Lib.is_modtype () then
@@ -327,7 +327,7 @@ let vernac_definition (local,_,_ as k) (loc,id as lid) def hook =
  	  declare_definition id k bl red_option c typ_opt hook)
  	      
 let vernac_start_proof kind l lettop hook =
-  if !Flags.dump then
+  if Dumpglob.dump () then
     List.iter (fun (id, _) -> 
       match id with
 	| Some lid -> Dumpglob.dump_definition lid false "prf"
@@ -366,14 +366,14 @@ let vernac_exact_proof c =
 let vernac_assumption kind l nl=
   let global = fst kind = Global in
     List.iter (fun (is_coe,(idl,c)) -> 
-      if !Flags.dump then
+      if Dumpglob.dump () then
 	List.iter (fun lid -> 
 	  if global then Dumpglob.dump_definition lid false "ax" 
 	  else Dumpglob.dump_definition lid true "var") idl;
       declare_assumption idl is_coe kind [] c false false nl) l
       
 let vernac_inductive f indl = 
-  if !Flags.dump then
+  if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, cstrs), _) ->
       Dumpglob.dump_definition lid false"ind";
       List.iter (fun (_, (lid, _)) ->
@@ -382,12 +382,12 @@ let vernac_inductive f indl =
   build_mutual indl f
 
 let vernac_fixpoint l b = 
-  if !Flags.dump then
+  if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   build_recursive l b
 
 let vernac_cofixpoint l b =
-  if !Flags.dump then
+  if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   build_corecursive l b
 
@@ -421,7 +421,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
     Modintern.interp_modtype Modintern.interp_modexpr
     id binders_ast (Some mty_ast_o) None
   in 
-    if !Flags.dump then Dumpglob.dump_moddef loc mp "mod";
+    if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "mod";
     if_verbose message ("Module "^ string_of_id id ^" is declared");
     Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
@@ -441,7 +441,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
        let mp = Declaremods.start_module Modintern.interp_modtype export
 	 id binders_ast mty_ast_o 
        in
-	 if !Flags.dump then Dumpglob.dump_moddef loc mp "mod";
+	 if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "mod";
 	 if_verbose message 
 	   ("Interactive Module "^ string_of_id id ^" started") ;
          List.iter
@@ -461,7 +461,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
 	  Modintern.interp_modtype Modintern.interp_modexpr
 	  id binders_ast mty_ast_o mexpr_ast_o 
        in
-	 if !Flags.dump then Dumpglob.dump_moddef loc mp "mod";
+	 if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "mod";
 	 if_verbose message 
 	   ("Module "^ string_of_id id ^" is defined");
          Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
@@ -469,7 +469,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
 
 let vernac_end_module export (loc,id) =
   let mp = Declaremods.end_module id in
-    if !Flags.dump then Dumpglob.dump_modref loc mp "mod";
+    if Dumpglob.dump () then Dumpglob.dump_modref loc mp "mod";
     if_verbose message ("Module "^ string_of_id id ^" is defined") ;
     Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
@@ -487,7 +487,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
            (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
              ([],[]) in
        let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in
-        if !Flags.dump then Dumpglob.dump_moddef loc mp "modtype";
+        if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "modtype";
 	if_verbose message 
 	  ("Interactive Module Type "^ string_of_id id ^" started");
         List.iter
@@ -506,14 +506,14 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
             else (idl,ty)) binders_ast in
 	let mp = Declaremods.declare_modtype Modintern.interp_modtype 
 	  id binders_ast base_mty in
-          if !Flags.dump then Dumpglob.dump_moddef loc mp "modtype";
+          if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "modtype";
 	  if_verbose message 
 	    ("Module Type "^ string_of_id id ^" is defined")
 
 
 let vernac_end_modtype (loc,id) =
   let mp = Declaremods.end_modtype id in
-    if !Flags.dump then Dumpglob.dump_modref loc mp "modtype";
+    if Dumpglob.dump () then Dumpglob.dump_modref loc mp "modtype";
     if_verbose message 
       ("Module Type "^ string_of_id id ^" is defined")
 
@@ -532,7 +532,7 @@ let vernac_record struc binders sort nameopt cfs =
   let const = match nameopt with 
     | None -> add_prefix "Build_" (snd (snd struc))
     | Some (_,id as lid) ->
-	if !Flags.dump then Dumpglob.dump_definition lid false "constr"; id in
+	if Dumpglob.dump () then Dumpglob.dump_definition lid false "constr"; id in
   let sigma = Evd.empty in
   let env = Global.env() in
   let s = interp_constr sigma env sort in
@@ -541,7 +541,7 @@ let vernac_record struc binders sort nameopt cfs =
     | Sort s -> s
     | _ -> user_err_loc
         (constr_loc sort,"definition_structure", str "Sort expected.") in
-    if !Flags.dump then (
+    if Dumpglob.dump () then (
       Dumpglob.dump_definition (snd struc) false "rec";
       List.iter (fun (_, x) ->
 	match x with
@@ -553,11 +553,11 @@ let vernac_record struc binders sort nameopt cfs =
 
 let vernac_begin_section (_, id as lid) =
   check_no_pending_proofs ();
-  if !Flags.dump then Dumpglob.dump_definition lid true "sec";
+  if Dumpglob.dump () then Dumpglob.dump_definition lid true "sec";
   Lib.open_section id
 
 let vernac_end_section (loc, id) = 
-  if !Flags.dump then 
+  if Dumpglob.dump () then 
     Dumpglob.dump_reference loc 
       (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
   Lib.close_section id
@@ -576,7 +576,7 @@ let vernac_require import _ qidl =
   let qidl = List.map qualid_of_reference qidl in
   let modrefl = List.map Library.try_locate_qualified_library qidl in
 (*   let modrefl = List.map (fun qid -> let (dp, _) = (Library.try_locate_qualified_library qid) in dp) qidl in *)
-    if !Flags.dump then
+    if Dumpglob.dump () then
       List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl);
     Library.require_library_from_dirpath modrefl import
 
@@ -597,21 +597,21 @@ let vernac_identity_coercion stre id qids qidt =
 
 (* Type classes *)
 let vernac_class id par ar sup props =
-  if !Flags.dump then (
+  if Dumpglob.dump () then (
       Dumpglob.dump_definition id false "class";
       List.iter (fun (lid, _, _) -> Dumpglob.dump_definition lid false "meth") props);
   Classes.new_class id par ar sup props
  
 let vernac_instance glob sup inst props pri =
-  if !Flags.dump then Dumpglob.dump_constraint inst false "inst";
+  if Dumpglob.dump () then Dumpglob.dump_constraint inst false "inst";
   ignore(Classes.new_instance ~global:glob sup inst props pri)
 
 let vernac_context l =
-  if !Flags.dump then List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
+  if Dumpglob.dump () then List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
   Classes.context l
 
 let vernac_declare_instance id =
-  if !Flags.dump then Dumpglob.dump_definition id false "inst";
+  if Dumpglob.dump () then Dumpglob.dump_definition id false "inst";
   Classes.declare_instance false id
 
 (***********)
@@ -746,7 +746,7 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef
 let vernac_hints = Auto.add_hints
 
 let vernac_syntactic_definition lid =
-  if !Flags.dump then Dumpglob.dump_definition lid false "syndef";
+  if Dumpglob.dump () then Dumpglob.dump_definition lid false "syndef";
   Command.syntax_definition (snd lid)
   
 let vernac_declare_implicits local r = function