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

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

Author: notin

Makefile.build

@@ -563,7 +563,7 @@ states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/M
 theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY)
 	$(SHOW)'COQC -nois $<'
 	$(HIDE)rm -f theories/Init/$*.glob
-	$(HIDE)$(BOOTCOQTOP) -dump-glob theories/Init/$*.glob -nois -compile theories/Init/$*
+	$(HIDE)$(BOOTCOQTOP) -nois -compile theories/Init/$*
 
 theories/Numbers/Natural/BigN/NMake.v: theories/Numbers/Natural/BigN/NMake_gen.ml
 	$(OCAML) $< > $@
@@ -875,7 +875,7 @@ endif
 %.vo %.glob: %.v states/initial.coq $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
 	$(SHOW)'COQC      $<'
 	$(HIDE)rm -f $*.glob 
-	$(HIDE)$(BOOTCOQTOP) -dump-glob $*.glob -compile $*
+	$(HIDE)$(BOOTCOQTOP) -compile $*
 ifdef VALIDATE
 	$(SHOW)'COQCHK    $(shell basename $*)'
 	$(HIDE)$(BESTCHICKEN) -silent -norec $(shell basename $*) \

Makefile.common

@@ -357,8 +357,8 @@ COQIDECMX:=$(COQIDECMO:.cmo=.cmx)
 COQMKTOPCMO:=$(CONFIG) scripts/tolink.cmo scripts/coqmktop.cmo 
 
 COQMKTOPCMX:=config/coq_config.cmx scripts/tolink.cmx scripts/coqmktop.cmx 
-COQCCMO:=$(CONFIG) toplevel/usage.cmo scripts/coqc.cmo
-COQCCMX:=config/coq_config.cmx toplevel/usage.cmx scripts/coqc.cmx
+COQCCMO:=$(CONFIG) toplevel/usage.cmo lib/pp_control.cmo lib/pp.cmo scripts/coqc.cmo
+COQCCMX:=config/coq_config.cmx toplevel/usage.cmx lib/pp_control.cmx lib/pp.cmx scripts/coqc.cmx
 
 INTERFACE:=\
   contrib/interface/vtp.cmo contrib/interface/xlate.cmo \

lib/flags.ml

@@ -84,6 +84,7 @@ let is_unsafe s = Stringset.mem s !unsafe_set
 
 (* Dump of globalization (to be used by coqdoc) *)
 
+let noglob = ref false
 let dump = ref false
 let dump_file = ref ""
 let dump_into_file f = dump := true; dump_file := f
@@ -94,9 +95,10 @@ let dump_string = Buffer.add_string dump_buffer
 
 let dump_it () = 
   if !dump then begin
-    let mode = [Open_wronly; Open_append; Open_creat] in
+    let mode = [Open_wronly; Open_creat] in
     let c = open_out_gen mode 0o666 !dump_file in
     output_string c (Buffer.contents dump_buffer);
+    Buffer.clear dump_buffer;
     close_out c
   end
 

lib/flags.mli

@@ -59,9 +59,11 @@ val is_unsafe : string -> bool
 
 (* Dump of globalization (to be used by coqdoc) *)
 
+val noglob : bool ref
 val dump : bool ref
 val dump_into_file : string -> unit
 val dump_string : string -> unit
+val dump_it : unit -> unit
 
 (* Options for the virtual machine *)
 

scripts/coqc.ml

@@ -141,7 +141,7 @@ let parse_args () =
     | ("-I"|"-include"|"-outputstate"
       |"-inputstate"|"-is"|"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
-      |"-init-file"|"-dump-glob" as o) :: rem ->
+      |"-init-file" as o) :: rem ->
 	begin
 	  match rem with
 	    | s :: rem' -> parse (cfiles,s::o::args) rem'
@@ -151,13 +151,16 @@ let parse_args () =
 
     | ("-notactics"|"-debug"|"-nolib"
       | "-debugVM"|"-alltransp"|"-VMno"
-      |"-batch"|"-nois"
+      |"-batch"|"-nois" | "-noglob" | "-no-glob"
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate" |"-strict-implicit"
       |"-dont-load-proofs"|"-impredicative-set"|"-vm" 
       | "-unboxed-values" | "-unboxed-definitions" | "-draw-vm-instr" 
 	  as o) :: rem ->
 	parse (cfiles,o::args) rem
+
+    | "-dump-glob" :: _ :: rem -> Pp.msg_warning (Pp.str "option -dumpglob is obsolete"); parse (cfiles,args) rem
+
     | "-where" :: _ -> 
 	let coqlib = 
 	  try Sys.getenv "COQLIB" with Not_found -> Coq_config.coqlib 

tools/coq_makefile.ml4

@@ -136,15 +136,15 @@ let implicit () =
     print "%.ml.d: %.ml\n";
     print "\t$(CAMLBIN)ocamldep -slash $(ZFLAGS) $(PP) \"$<\" > \"$@\"\n\n"
   and v_rule () =
-    print "%.vo %.glob: %.v\n\t$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*\n\n";
+    print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
     print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
     print "%.g: %.v\n\t$(GALLINA) $<\n\n";
     print "%.tex: %.v\n\t$(COQDOC) -latex $< -o $@\n\n";
-    print "%.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob  -html $< -o $@\n\n";
+    print "%.html: %.v %.glob\n\t$(COQDOC) -html $< -o $@\n\n";
     print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n";
-    print "%.g.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html -g $< -o $@\n\n";
+    print "%.g.html: %.v %.glob\n\t$(COQDOC) -html -g $< -o $@\n\n";
     print "%.v.d: %.v\n";
-    print "\t$(COQDEP) -glob -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
+    print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
   in
     if !some_mlfile then ml_rules ();
     if !some_vfile then v_rule ()

tools/coqdep.ml

@@ -22,7 +22,7 @@ let option_D = ref false
 let option_w = ref false
 let option_i = ref false
 let option_sort = ref false
-let option_glob = ref false
+let option_noglob = ref false
 let option_slash = ref false
 let option_boot = ref false
 
@@ -375,7 +375,7 @@ let mL_dependencies () =
 let coq_dependencies () =
   List.iter
     (fun (name,_) ->
-       let glob = if !option_glob then " "^name^".glob" else "" in 
+       let glob = if !option_noglob then "" else " "^name^".glob" in 
        printf "%s%s%s: %s.v" name !suffixe glob name;
        traite_fichier_Coq true (name ^ ".v");
        printf "\n";
@@ -503,7 +503,7 @@ let rec parse = function
   | "-i" :: ll -> option_i := true; parse ll
   | "-boot" :: ll -> option_boot := true; parse ll
   | "-sort" :: ll -> option_sort := true; parse ll
-  | "-glob" :: ll -> option_glob := true; parse ll
+  | "-noglob" :: ll | "-no-glob" :: ll -> option_noglob := true; parse ll
   | "-I" :: r :: ll -> add_dir add_known r []; parse ll
   | "-I" :: [] -> usage ()
   | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll

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 ()

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

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")
+