summaryrefslogtreecommitdiff
path: root/tools/coqdoc/main.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/main.ml')
-rw-r--r--tools/coqdoc/main.ml280
1 files changed, 156 insertions, 124 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 2ee9ac96..67c63865 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: main.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id$ i*)
(* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
* - handling of absolute filenames (function coq_module)
@@ -46,6 +46,7 @@ let usage () =
prerr_endline " --with-footer <file> append <file> as html footer";
prerr_endline " --no-index do not output the index";
prerr_endline " --multi-index index split in multiple files";
+ prerr_endline " --index <string> set index name (default is index)";
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";
@@ -53,8 +54,9 @@ let usage () =
prerr_endline " --files-from <file> read file names to process in <file>";
prerr_endline " --glob-from <file> read globalization information from <file>";
prerr_endline " --quiet quiet mode (default)";
- prerr_endline " --verbose verbose mode";
+ prerr_endline " --verbose verbose mode";
prerr_endline " --no-externals no links to Coq standard library";
+ prerr_endline " --external <url> <d> set URL for external library d";
prerr_endline " --coqlib <url> set URL for Coq standard library";
prerr_endline (" (default is " ^ Coq_config.wwwstdlib ^ ")");
prerr_endline " --boot run in boot mode";
@@ -66,6 +68,11 @@ let usage () =
prerr_endline " --inputenc <string> set LaTeX input encoding";
prerr_endline " --interpolate try to typeset identifiers in comments using definitions in the same module";
prerr_endline " --parse-comments parse regular comments";
+ prerr_endline " --plain-comments consider comments as non-literate text";
+ prerr_endline " --toc-depth <int> don't include TOC entries for sections below level <int>";
+ prerr_endline " --no-lib-name don't display \"Library\" before library names in the toc";
+ prerr_endline " --lib-name <string> call top level toc entries <string> instead of \"Library\"";
+ prerr_endline " --lib-subtitles first line comments of the form (** * ModuleName : text *) will be interpreted as subtitles";
prerr_endline "";
exit 1
@@ -74,20 +81,20 @@ let obsolete 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
+ is not (unless both standard and error outputs are redirected, of
course). *)
let banner () =
eprintf "This is coqdoc version %s, compiled on %s\n"
Coq_config.version Coq_config.compile_date;
flush stderr
-
-let target_full_name f =
+
+let target_full_name f =
match !Cdglobals.target_language with
| HTML -> f ^ ".html"
| Raw -> f ^ ".txt"
| _ -> f ^ ".tex"
-
+
(*s \textbf{Separation of files.} Files given on the command line are
separated according to their type, which is determined by their
suffix. Coq files have suffixe \verb!.v! or \verb!.g! and \LaTeX\
@@ -95,12 +102,12 @@ let target_full_name f =
let check_if_file_exists f =
if not (Sys.file_exists f) then begin
- eprintf "\ncoqdoc: %s: no such file\n" f;
+ eprintf "coqdoc: %s: no such file\n" f;
exit 1
end
-(*s Manipulations of paths and path aliases *)
+(*s Manipulations of paths and path aliases *)
let normalize_path p =
(* We use the Unix subsystem to normalize a physical path (relative
@@ -109,50 +116,43 @@ let normalize_path p =
works... *)
(* Rq: Sys.getcwd () returns paths without '/' at the end *)
let orig = Sys.getcwd () in
- Sys.chdir p;
- let res = Sys.getcwd () in
- Sys.chdir orig;
- res
+ Sys.chdir p;
+ let res = Sys.getcwd () in
+ Sys.chdir orig;
+ res
let normalize_filename f =
let basename = Filename.basename f in
let dirname = Filename.dirname f in
- Filename.concat (normalize_path dirname) basename
+ normalize_path dirname, basename
(* [paths] maps a physical path to a name *)
let paths = ref []
-
-let add_path dir name =
- (* if dir is relative we add both the relative and absolute name *)
+
+let add_path dir name =
let p = normalize_path dir in
- paths := (p,name) :: !paths
-
-(* turn A/B/C into A.B.C *)
-let name_of_path = Str.global_replace (Str.regexp "/") ".";;
+ paths := (p,name) :: !paths
-let coq_module filename =
+(* turn A/B/C into A.B.C *)
+let rec name_of_path p name dirname suffix =
+ if p = dirname then String.concat "." (name::suffix)
+ else
+ let subdir = Filename.dirname dirname in
+ if subdir = dirname then raise Not_found
+ else name_of_path p name subdir (Filename.basename dirname::suffix)
+
+let coq_module filename =
let bfname = Filename.chop_extension filename in
- let nfname = normalize_filename bfname in
- let rec change_prefix map f =
- match map with
- | [] ->
- (* There is no prefix alias;
- we just cut the name wrt current working directory *)
- let cwd = Sys.getcwd () in
- let exp = Str.regexp (Str.quote (cwd ^ "/")) in
- if (Str.string_match exp f 0) then
- name_of_path (Str.replace_first exp "" f)
- else
- name_of_path f
- | (p, name) :: rem ->
- let expp = Str.regexp (Str.quote p) in
- if (Str.string_match expp f 0) then
- let newp = Str.replace_first expp name f in
- name_of_path newp
- else
- change_prefix rem f
+ let dirname, fname = normalize_filename bfname in
+ let rec change_prefix = function
+ (* Follow coqc: if in scope of -R, substitute logical name *)
+ (* otherwise, keep only base name *)
+ | [] -> fname
+ | (p, name) :: rem ->
+ try name_of_path p name dirname [fname]
+ with Not_found -> change_prefix rem
in
- change_prefix !paths nfname
+ change_prefix !paths
let what_file f =
check_if_file_exists f;
@@ -160,10 +160,10 @@ let what_file f =
Vernac_file (f, coq_module f)
else if Filename.check_suffix f ".tex" then
Latex_file f
- else
+ else
(eprintf "\ncoqdoc: don't know what to do with %s\n" f; exit 1)
-
-(*s \textbf{Reading file names from a file.}
+
+(*s \textbf{Reading file names from a file.}
* File names may be given
* in a file instead of being given on the command
* line. [(files_from_file f)] returns the list of file names contained
@@ -181,7 +181,7 @@ let files_from_file f =
| ' ' | '\t' | '\n' ->
if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l;
Buffer.clear buf
- | c ->
+ | c ->
Buffer.add_char buf c
done; []
with End_of_file ->
@@ -193,12 +193,12 @@ let files_from_file f =
let l = files_from_channel ch in
close_in ch;l
with Sys_error s -> begin
- eprintf "\ncoqdoc: cannot read from file %s (%s)\n" f s;
+ eprintf "coqdoc: cannot read from file %s (%s)\n" f s;
exit 1
end
-
+
(*s \textbf{Parsing of the command line.} *)
-
+
let dvi = ref false
let ps = ref false
let pdf = ref false
@@ -208,7 +208,7 @@ let parse () =
let add_file f = files := f :: !files in
let rec parse_rec = function
| [] -> ()
-
+
| ("-nopreamble" | "--nopreamble" | "--no-preamble"
| "-bodyonly" | "--bodyonly" | "--body-only") :: rem ->
header_trailer := false; parse_rec rem
@@ -228,17 +228,21 @@ let parse () =
index := false; parse_rec rem
| ("-multi-index" | "--multi-index") :: rem ->
multi_index := true; parse_rec rem
+ | ("-index" | "--index") :: s :: rem ->
+ Cdglobals.index_name := s; parse_rec rem
+ | ("-index" | "--index") :: [] ->
+ usage ()
| ("-toc" | "--toc" | "--table-of-contents") :: rem ->
toc := true; parse_rec rem
| ("-stdout" | "--stdout") :: rem ->
out_to := StdOut; parse_rec rem
| ("-o" | "--output") :: f :: rem ->
out_to := File (Filename.basename f); output_dir := Filename.dirname f; parse_rec rem
- | ("-o" | "--output") :: [] ->
+ | ("-o" | "--output") :: [] ->
usage ()
| ("-d" | "--directory") :: dir :: rem ->
output_dir := dir; parse_rec rem
- | ("-d" | "--directory") :: [] ->
+ | ("-d" | "--directory") :: [] ->
usage ()
| ("-s" | "--short") :: rem ->
short := true; parse_rec rem
@@ -276,39 +280,60 @@ let parse () =
Cdglobals.raw_comments := true; parse_rec rem
| ("-parse-comments" | "--parse-comments") :: rem ->
Cdglobals.parse_comments := true; parse_rec rem
+ | ("-plain-comments" | "--plain-comments") :: rem ->
+ Cdglobals.plain_comments := true; parse_rec rem
| ("-interpolate" | "--interpolate") :: rem ->
Cdglobals.interpolate := true; parse_rec rem
+ | ("-toc-depth" | "--toc-depth") :: [] ->
+ usage ()
+ | ("-toc-depth" | "--toc-depth") :: ds :: rem ->
+ let d = try int_of_string ds with
+ Failure _ ->
+ (eprintf "--toc-depth must be followed by an integer\n";
+ exit 1)
+ in
+ Cdglobals.toc_depth := Some d;
+ parse_rec rem
+ | ("-no-lib-name" | "--no-lib-name") :: rem ->
+ Cdglobals.lib_name := "";
+ parse_rec rem
+ | ("-lib-name" | "--lib-name") :: ds :: rem ->
+ Cdglobals.lib_name := ds;
+ parse_rec rem
+ | ("-lib-subtitles" | "--lib-subtitles") :: rem ->
+ Cdglobals.lib_subtitles := true;
+ parse_rec rem
| ("-latin1" | "--latin1") :: rem ->
Cdglobals.set_latin1 (); parse_rec rem
| ("-utf8" | "--utf8") :: rem ->
Cdglobals.set_utf8 (); parse_rec rem
-
+
| ("-q" | "-quiet" | "--quiet") :: rem ->
quiet := true; parse_rec rem
| ("-v" | "-verbose" | "--verbose") :: rem ->
quiet := false; parse_rec rem
-
+
| ("-h" | "-help" | "-?" | "--help") :: rem ->
banner (); usage ()
| ("-V" | "-version" | "--version") :: _ ->
banner (); exit 0
- | ("-vernac-file" | "--vernac-file") :: f :: rem ->
+ | ("-vernac-file" | "--vernac-file") :: f :: rem ->
check_if_file_exists f;
add_file (Vernac_file (f, coq_module f)); parse_rec rem
| ("-vernac-file" | "--vernac-file") :: [] ->
usage ()
- | ("-tex-file" | "--tex-file") :: f :: rem ->
+ | ("-tex-file" | "--tex-file") :: f :: rem ->
add_file (Latex_file f); parse_rec rem
| ("-tex-file" | "--tex-file") :: [] ->
usage ()
| ("-files" | "--files" | "--files-from") :: f :: rem ->
- List.iter (fun f -> add_file (what_file f)) (files_from_file f);
+ List.iter (fun f -> add_file (what_file f)) (files_from_file f);
parse_rec rem
| ("-files" | "--files") :: [] ->
usage ()
- | "-R" :: path :: log :: rem ->
+ | "-R" :: path :: log :: rem ->
add_path path log; parse_rec rem
| "-R" :: ([] | [_]) ->
usage ()
@@ -318,6 +343,8 @@ let parse () =
usage ()
| ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
Cdglobals.externals := false; parse_rec rem
+ | ("--external" | "-external") :: u :: logicalpath :: rem ->
+ Index.add_external_library logicalpath u; parse_rec rem
| ("--coqlib" | "-coqlib") :: u :: rem ->
Cdglobals.coqlib := u; parse_rec rem
| ("--coqlib" | "-coqlib") :: [] ->
@@ -328,16 +355,15 @@ let parse () =
Cdglobals.coqlib_path := d; parse_rec rem
| ("--coqlib_path" | "-coqlib_path") :: [] ->
usage ()
- | f :: rem ->
+ | f :: rem ->
add_file (what_file f); parse_rec rem
- in
+ in
parse_rec (List.tl (Array.to_list Sys.argv));
- Output.initialize ();
List.rev !files
-
+
(*s The following function produces the output. The default output is
- the \LaTeX\ document: in that case, we just call [Web.produce_document].
+ the \LaTeX\ document: in that case, we just call [Web.produce_document].
If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then
we make calls to \verb!latex! or \verb!dvips! or \verb!pdflatex! accordingly. *)
@@ -359,9 +385,9 @@ let clean_temp_files basefile =
remove (basefile ^ ".pdf");
remove (basefile ^ ".haux");
remove (basefile ^ ".html")
-
+
let clean_and_exit file res = clean_temp_files file; exit res
-
+
let cat file =
let c = open_in file in
try
@@ -370,20 +396,26 @@ let cat file =
close_in c
let copy src dst =
- let cin = open_in src
- and cout = open_out dst in
+ let cin = open_in src in
+ try
+ let cout = open_out dst in
try
while true do Pervasives.output_char cout (input_char cin) done
with End_of_file ->
- close_in cin; close_out cout
-
+ close_out cout;
+ close_in cin
+ with Sys_error e ->
+ eprintf "%s\n" e;
+ exit 1
(*s Functions for generating output files *)
let gen_one_file l =
let file = function
- | Vernac_file (f,m) ->
- Output.set_module m; Pretty.coq_file f m
+ | Vernac_file (f,m) ->
+ let sub = if !lib_subtitles then Cpretty.detect_subtitle f m else None in
+ Output.set_module m sub;
+ Cpretty.coq_file f m
| Latex_file _ -> ()
in
if (!header_trailer) then Output.header ();
@@ -391,74 +423,73 @@ let gen_one_file l =
List.iter file l;
if !index then Output.make_index();
if (!header_trailer) then Output.trailer ()
-
+
let gen_mult_files l =
let file = function
- | Vernac_file (f,m) ->
- Output.set_module m;
+ | Vernac_file (f,m) ->
+ let sub = if !lib_subtitles then Cpretty.detect_subtitle f m else None in
let hf = target_full_name m in
+ Output.set_module m sub;
open_out_file hf;
- if (!header_trailer) then Output.header ();
- Pretty.coq_file f m;
+ if (!header_trailer) then Output.header ();
+ Cpretty.coq_file f m;
if (!header_trailer) then Output.trailer ();
close_out_file()
| Latex_file _ -> ()
in
List.iter file l;
if (!index && !target_language=HTML) then begin
- if (!multi_index) then Output.make_multi_index ();
- open_out_file "index.html";
+ if (!multi_index) then Output.make_multi_index ();
+ open_out_file (!index_name^".html");
page_title := (if !title <> "" then !title else "Index");
- if (!header_trailer) then Output.header ();
- Output.make_index ();
+ if (!header_trailer) then Output.header ();
+ Output.make_index ();
if (!header_trailer) then Output.trailer ();
close_out_file()
end;
if (!toc && !target_language=HTML) then begin
- open_out_file "toc.html";
+ open_out_file "toc.html";
page_title := (if !title <> "" then !title else "Table of contents");
if (!header_trailer) then Output.header ();
if !title <> "" then printf "<h1>%s</h1>\n" !title;
- Output.make_toc ();
+ Output.make_toc ();
if (!header_trailer) then Output.trailer ();
close_out_file()
- end
+ end
(* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
-let read_glob x =
- match x with
- | Vernac_file (f,m) ->
- let glob = (Filename.chop_extension f) ^ ".glob" in
- (try
- Vernac_file (f, Index.read_glob glob)
- with e ->
- eprintf "Warning: file %s cannot be used; links will not be available: %s\n" glob (Printexc.to_string e);
- x)
- | Latex_file _ -> x
+let read_glob_file x =
+ try Index.read_glob x
+ with Sys_error s ->
+ eprintf "Warning: %s (links will not be available)\n" s
+
+let read_glob_file_of = function
+ | Vernac_file (f,_) -> read_glob_file (Filename.chop_extension f ^ ".glob")
+ | Latex_file _ -> ()
let index_module = function
- | Vernac_file (f,m) ->
+ | Vernac_file (f,m) ->
Index.add_module m
| Latex_file _ -> ()
-
+
+let copy_style_file file =
+ let src =
+ List.fold_left
+ Filename.concat !Cdglobals.coqlib_path ["tools";"coqdoc";file] in
+ let dst = coqdoc_out file in
+ if Sys.file_exists src then copy src dst
+ else eprintf "Warning: file %s does not exist\n" src
+
let produce_document l =
- (if !target_language=HTML then
- let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in
- let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in
- if (Sys.file_exists src) then (copy src dst) else eprintf "Warning: file %s does not exist\n" src);
- (if !target_language=LaTeX then
- let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
- let dst = if !output_dir <> "" then
- Filename.concat !output_dir "coqdoc.sty"
- else "coqdoc.sty" in
- if Sys.file_exists src then copy src dst else eprintf "Warning: file %s does not exist\n" src);
+ if !target_language=HTML then copy_style_file "coqdoc.css";
+ if !target_language=LaTeX then copy_style_file "coqdoc.sty";
(match !Cdglobals.glob_source with
| NoGlob -> ()
- | DotGlob -> ignore (List.map read_glob l)
- | GlobFile f -> ignore (Index.read_glob f));
+ | DotGlob -> List.iter read_glob_file_of l
+ | GlobFile f -> read_glob_file f);
List.iter index_module l;
match !out_to with
- | StdOut ->
+ | StdOut ->
Cdglobals.out_channel := stdout;
gen_one_file l
| File f ->
@@ -467,11 +498,11 @@ let produce_document l =
close_out_file()
| MultFiles ->
gen_mult_files l
-
+
let produce_output fl =
- if not (!dvi || !ps || !pdf) then
+ if not (!dvi || !ps || !pdf) then
produce_document fl
- else
+ else
begin
let texfile = Filename.temp_file "coqdoc" ".tex" in
let basefile = Filename.chop_suffix texfile ".tex" in
@@ -479,52 +510,52 @@ let produce_output fl =
out_to := File texfile;
output_dir := (Filename.dirname texfile);
produce_document fl;
-
+
let latexexe = if !pdf then "pdflatex" else "latex" in
- let latexcmd =
+ let latexcmd =
let file = Filename.basename texfile in
- let file =
- if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file
+ let file =
+ if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file
in
sprintf "%s %s && %s %s 1>&2 %s" latexexe file latexexe file (if !quiet then "> /dev/null" else "")
in
let res = locally (Filename.dirname texfile) Sys.command latexcmd in
if res <> 0 then begin
- eprintf "Couldn't run LaTeX successfully\n";
+ eprintf "Couldn't run LaTeX successfully\n";
clean_and_exit basefile res
end;
-
+
let dvifile = basefile ^ ".dvi" in
- if !dvi then
+ if !dvi then
begin
match final_out_to with
| MultFiles | StdOut -> cat dvifile
| File f -> copy dvifile f
end;
let pdffile = basefile ^ ".pdf" in
- if !pdf then
+ if !pdf then
begin
match final_out_to with
| MultFiles | StdOut -> cat pdffile
| File f -> copy pdffile f
end;
if !ps then begin
- let psfile = basefile ^ ".ps"
+ let psfile = basefile ^ ".ps"
in
- let command =
- sprintf "dvips %s -o %s %s" dvifile psfile
+ let command =
+ sprintf "dvips %s -o %s %s" dvifile psfile
(if !quiet then "> /dev/null 2>&1" else "")
in
let res = Sys.command command in
if res <> 0 then begin
- eprintf "Couldn't run dvips successfully\n";
+ eprintf "Couldn't run dvips successfully\n";
clean_and_exit basefile res
end;
match final_out_to with
| MultFiles | StdOut -> cat psfile
| File f -> copy psfile f
end;
-
+
clean_temp_files basefile
end
@@ -534,7 +565,8 @@ let produce_output fl =
let main () =
let files = parse () in
+ Index.init_coqlib_library ();
if not !quiet then banner ();
if files <> [] then produce_output files
-
+
let _ = Printexc.catch main ()
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 07:40:42 +0000