diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-26 16:43:15 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-26 16:43:15 +0000 |
commit | 286432aabdb7c7ce43f7d98202e1a2f560885be0 (patch) | |
tree | b1d5d3ae57660ac616a5363b4e5a9c2f20327839 /tools | |
parent | e31e4f88b20d7c32030ef6c0fe711f5fb7de2f66 (diff) |
Ajout option raw-comments pour supprimer affichage de <table>; typos
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5579 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r-- | tools/coqdoc/main.ml | 65 |
1 files changed, 33 insertions, 32 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 68eb76576..099eb6e0d 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -28,37 +28,36 @@ open Pretty let usage () = prerr_endline ""; prerr_endline "Usage: coqdoc <options and files>"; - prerr_endline " --html produce a HTML document (default)"; - prerr_endline " --latex produce a LaTeX document"; - prerr_endline " --texmacs produce a TeXmacs document"; - prerr_endline " --dvi output the DVI"; - prerr_endline " --ps output the PostScript"; - prerr_endline " -o <file> write output in file <file>"; - prerr_endline " (only with -latex, -dvi or -ps)"; - prerr_endline " -d <dir> output files into directory <dir>"; - prerr_endline " -g (gallina) skip proofs"; - prerr_endline " -s (short) no titles for files"; - prerr_endline " -l light mode (only defs and statements)"; - prerr_endline " -t <string> give a title to the document"; - prerr_endline " --body-only suppress LaTeX/HTML header and trailer"; - prerr_endline " --no-index do not output the index"; - prerr_endline " --mutli-index index split in multiple files"; - prerr_endline " --toc output a table of contents"; - prerr_endline " --vernac <file> consider <file> as a .v file"; - prerr_endline " --tex <file> consider <file> as a .tex file"; - prerr_endline " -p <string> insert <string> in LaTeX preamble"; - prerr_endline " --files-from <file>"; - prerr_endline " read file names to process in <file>"; - prerr_endline " --quiet quiet mode"; - prerr_endline " --glob-from <f> read Coq globalizations from file <f>"; - 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/)"; - prerr_endline " -R dir coqdir map physical dir to Coq dir"; - prerr_endline " --latin1 set ISO-8859-1 input language"; - prerr_endline " --utf8 set UTF-8 input language"; - prerr_endline " --charset set HTML charset"; - prerr_endline " --inputenc set LaTeX input encoding"; + prerr_endline " --html produce a HTML document (default)"; + prerr_endline " --latex produce a LaTeX document"; + prerr_endline " --texmacs produce a TeXmacs document"; + prerr_endline " --dvi output the DVI"; + prerr_endline " --ps output the PostScript"; + prerr_endline " -o <file> write output in file <file>"; + prerr_endline " -d <dir> output files into directory <dir>"; + prerr_endline " -g (gallina) skip proofs"; + prerr_endline " -s (short) no titles for files"; + prerr_endline " -l light mode (only defs and statements)"; + prerr_endline " -t <string> give a title to the document"; + prerr_endline " --body-only suppress LaTeX/HTML header and trailer"; + prerr_endline " --no-index do not output the index"; + prerr_endline " --multi-index index split in multiple files"; + prerr_endline " --toc output a table of contents"; + prerr_endline " --vernac <file> consider <file> as a .v file"; + prerr_endline " --tex <file> consider <file> as a .tex file"; + prerr_endline " -p <string> insert <string> in LaTeX preamble"; + prerr_endline " --files-from <file> read file names to process in <file>"; + prerr_endline " --quiet quiet 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/)"; + prerr_endline " -R <dir> <coqdir> map physical dir to Coq dir"; + prerr_endline " --latin1 set ISO-8859-1 input language"; + prerr_endline " --utf8 set UTF-8 input language"; + prerr_endline " --charset <string> set HTML charset"; + prerr_endline " --inputenc <string> set LaTeX input encoding"; + prerr_endline " --raw-comments don't insert comments in table"; prerr_endline ""; prerr_endline "On-line documentation at http://www.lri.fr/~filliatr/coqdoc/\n"; @@ -271,7 +270,9 @@ let parse () = Output.inputenc := s; parse_rec rem | ("-inputenc" | "--inputenc") :: [] -> usage () - | ("-latin1" | "--latin1") :: rem -> + | ("-raw-comments" | "--raw-comments") :: rem -> + Output.raw_comments := true; parse_rec rem + | ("-latin1" | "--latin1") :: rem -> Output.set_latin1 (); parse_rec rem | ("-utf8" | "--utf8") :: rem -> Output.set_utf8 (); parse_rec rem |