1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Printf
open Common
(*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
course). *)
let banner () =
eprintf "This is coqdoc version %s\n" Coq_config.version;
flush stderr
let target_full_name f =
match !prefs.targetlang with
| HTML -> f ^ ".html"
| Raw -> f ^ ".txt"
| _ -> f ^ ".tex"
(*s The following function produces the output. The default output is
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. *)
(*s Functions for generating output files *)
let gen_one_file l =
let file = function
| Vernac_file (f,m) ->
let sub = if !prefs.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 (!prefs.header_trailer) then Output.header ();
if !prefs.toc then Output.make_toc ();
List.iter file l;
if !prefs.index then Output.make_index();
if (!prefs.header_trailer) then Output.trailer ()
let gen_mult_files l =
let file = function
| Vernac_file (f,m) ->
let sub = if !prefs.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 (!prefs.header_trailer) then Output.header ();
Cpretty.coq_file f m;
if (!prefs.header_trailer) then Output.trailer ();
close_out_file()
| Latex_file _ -> ()
in
List.iter file l;
if (!prefs.index && !prefs.targetlang=HTML) then begin
if (!prefs.multi_index) then Output.make_multi_index ();
open_out_file (!prefs.index_name^".html");
page_title := (if !prefs.title <> "" then !prefs.title else "Index");
if (!prefs.header_trailer) then Output.header ();
Output.make_index ();
if (!prefs.header_trailer) then Output.trailer ();
close_out_file()
end;
if (!prefs.toc && !prefs.targetlang=HTML) then begin
open_out_file "toc.html";
page_title := (if !prefs.title <> "" then !prefs.title else "Table of contents");
if (!prefs.header_trailer) then Output.header ();
if !prefs.title <> "" then printf "<h1>%s</h1>\n" !prefs.title;
Output.make_toc ();
if (!prefs.header_trailer) then Output.trailer ();
close_out_file()
end
(* NB: for latex and texmacs, a separated toc or index is meaningless... *)
let read_glob_file vfile f =
try Glob_file.read_glob vfile f
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 (Some f) (Filename.chop_extension f ^ ".glob")
| Latex_file _ -> ()
let index_module = function
| Vernac_file (f,m) ->
Index.add_module m
| Latex_file _ -> ()
module E = Boot.Env
let copy_style_file file =
(* We give preference to coqlib in case it is overriden *)
let env = E.init () in
let coqdoc = E.tool env "coqdoc" in
let sty_file = E.Path.relative coqdoc file in
if not (E.Path.exists sty_file) then
begin
let sty_file = E.Path.to_string sty_file in
eprintf "coqdoc: cannot find coqdoc style file: %s\n" sty_file;
exit 1
end;
let sty_file_s = E.Path.to_string sty_file in
let dst = coqdoc_out file in
FileUtil.copy sty_file_s dst
let produce_document l =
if !prefs.targetlang=HTML then copy_style_file "coqdoc.css";
if !prefs.targetlang=LaTeX then copy_style_file "coqdoc.sty";
(match !prefs.glob_source with
| NoGlob -> ()
| DotGlob -> List.iter read_glob_file_of l
| GlobFile f -> read_glob_file None f);
List.iter index_module l;
match !prefs.out_to with
| StdOut ->
Common.out_channel := stdout;
gen_one_file l
| File f ->
open_out_file f;
gen_one_file l;
close_out_file()
| MultFiles ->
gen_mult_files l
let produce_output fl =
if List.length !prefs.compile_targets = 0 then
produce_document fl
else
let otypes = !prefs.compile_targets in
LatexCompiler.compile ~otypes ~produce_document fl
(*s \textbf{Main program.} Print the banner, parse the command line,
read the files and then call [produce_document] from module [Web]. *)
let _ =
CmdArgs.parse_args (); (* Sets prefs *)
let files = List.rev !prefs.files in
Index.init_coqlib_library ();
if not !prefs.quiet then banner ();
if files <> [] then produce_output files
|
