Suppression de l'option -glob-from de Coqdoc: les globalisations sont

lues directement des fichiers .glob



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

2 files changed, 13 insertions, 11 deletions

diff --git a/doc/Makefile b/doc/Makefile
index b6290ff0cb..6e606ed194 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -214,8 +214,6 @@ faq/html/index.html: faq/FAQ.v.html
 # Standard library
 ######################################################################
 
-GLOBDUMP=$(COQSRC)/glob.dump
-
 LIBDIRS= Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals Program
 # We avoid Strings as String.v contains unicode caracters that make latex fail
 
@@ -229,14 +227,11 @@ ALLTHEORIES_GLOB = $(ALLTHEORIES_V:%.v=%.glob)
 
 ### Standard library (browsable html format)
 
-$(GLOBDUMP): $(ALLTHEORIES_GLOB)
-	$(MAKE) -C .. $(@:../%=%)
-
-stdlib/index-body.html: $(GLOBDUMP) $(ALLTHEORIES_V)
+stdlib/index-body.html: $(ALLTHEORIES_V)
 	- rm -rf stdlib/html
 	mkdir stdlib/html
 	(cd stdlib/html;\
-	 $(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\
+	 $(COQDOC) -q --multi-index --html \
 	  -R $(COQSRC)/theories Coq $(ALLTHEORIES_V))
 	mv stdlib/html/index.html stdlib/index-body.html
 
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 7c97055a67..c3a32f08ff 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -51,7 +51,6 @@ let usage () =
   prerr_endline "  --files-from <file> read file names to process in <file>";
   prerr_endline "  --quiet             quiet mode (default)";
   prerr_endline "  --verbose           verbose mode";  
-  prerr_endline "  --glob-from <file>  read Coq globalizations from file <file>";
   prerr_endline "  --no-externals      no links to Coq standard library";
   prerr_endline "  --coqlib <url>      set URL for Coq standard library";
   prerr_endline "                      (default is http://coq.inria.fr/library/)";
@@ -64,6 +63,9 @@ let usage () =
   prerr_endline "";
   exit 1
 
+let obsolete s =
+  eprintf "Warning: option %s is now obsolete; please update your scripts\n" s
+
 (*s \textbf{Banner.} Always printed. Notice that it is printed on error
     output, so that when the output of [coqdoc] is redirected this header
     is not (unless both standard and error outputs are redirected, of 
@@ -311,7 +313,7 @@ let parse () =
     | "-R" :: ([] | [_]) ->
 	usage ()
     | ("-glob-from" | "--glob-from") :: f :: rem ->
-	Index.read_glob f; parse_rec rem
+	obsolete "glob-from"; parse_rec rem
     | ("-glob-from" | "--glob-from") :: [] ->
 	usage ()
     | ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
@@ -372,7 +374,7 @@ let copy src dst =
 
 
 (*s Functions for generating output files *)
-	
+
 let gen_one_file l =
   let file = function
     | Vernac_file (f,m) -> 
@@ -420,8 +422,13 @@ let gen_mult_files l =
       (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
 
 
+let glob_filename f =
+  (Filename.chop_extension f) ^ ".glob"
+    
 let index_module = function
-  | Vernac_file (_,m) -> Index.add_module m
+  | Vernac_file (f,m) ->   
+      Index.read_glob (glob_filename f);
+      Index.add_module m
   | Latex_file _ -> ()
       
 let produce_document l =