From d6f4f3f3dc92d805bc046bcdbc30dd7df65fb4aa Mon Sep 17 00:00:00 2001 From: notin Date: Fri, 18 Jul 2008 15:58:12 +0000 Subject: Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from de coqdoc (compatibilité) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tools/coqdoc/cdglobals.ml | 7 +++++++ tools/coqdoc/main.ml | 8 ++++++-- 2 files changed, 13 insertions(+), 2 deletions(-) (limited to 'tools') diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 44b9bd3ce..3339b1dba 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -32,6 +32,13 @@ let open_out_file f = let close_out_file () = close_out !out_channel +type glob_source_t = + | NoGlob + | DotGlob + | GlobFile of string + +let glob_source = ref DotGlob + let header_trailer = ref true let header_file = ref "" let header_file_spec = ref false diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 7466a6ba1..d9384adc4 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -50,6 +50,7 @@ let usage () = prerr_endline " --tex consider as a .tex file"; prerr_endline " -p insert in LaTeX preamble"; prerr_endline " --files-from read file names to process in "; + prerr_endline " --glob-from read globalization information from "; prerr_endline " --quiet quiet mode (default)"; prerr_endline " --verbose verbose mode"; prerr_endline " --no-externals no links to Coq standard library"; @@ -300,7 +301,7 @@ let parse () = | "-R" :: ([] | [_]) -> usage () | ("-glob-from" | "--glob-from") :: f :: rem -> - obsolete "glob-from"; parse_rec rem + glob_source := GlobFile f; parse_rec rem | ("-glob-from" | "--glob-from") :: [] -> usage () | ("--no-externals" | "-no-externals" | "-noexternals") :: rem -> @@ -436,7 +437,10 @@ let produce_document l = Filename.concat !output_dir "coqdoc.sty" else "coqdoc.sty" in copy src dst); - let l = List.map read_glob l in + (match !Cdglobals.glob_source with + | NoGlob -> () + | DotGlob -> ignore (List.map read_glob l) + | GlobFile f -> ignore (Index.read_glob f)); List.iter index_module l; match !out_to with | StdOut -> -- cgit v1.2.3