blob: b356ac537be324e7ee3e0eb74bd9611175a4fffc (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*s Output options *)
type target_language = LaTeX | HTML | TeXmacs | Raw
let target_language = ref HTML
type output_t =
| StdOut
| MultFiles
| File of string
let output_dir = ref ""
let out_to = ref MultFiles
let out_channel = ref stdout
let ( / ) = Filename.concat
let coqdoc_out f =
if !output_dir <> "" && Filename.is_relative f then
if not (Sys.file_exists !output_dir) then
(Printf.eprintf "No such directory: %s\n" !output_dir; exit 1)
else
!output_dir / f
else
f
let open_out_file f =
out_channel :=
try open_out (coqdoc_out f)
with Sys_error s -> Printf.eprintf "%s\n" s; exit 1
let close_out_file () = close_out !out_channel
type glob_source_t =
| NoGlob
| DotGlob
| GlobFile of string
let glob_source = ref DotGlob
(*s Manipulations of paths and path aliases *)
let normalize_path p =
(* We use the Unix subsystem to normalize a physical path (relative
or absolute) and get rid of symbolic links, relative links (like
./ or ../ in the middle of the path; it's tricky but it
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
let normalize_filename f =
let basename = Filename.basename f in
let dirname = Filename.dirname f in
normalize_path dirname, basename
(** A weaker analog of the function in Envars *)
let guess_coqlib () =
let file = "theories/Init/Prelude.vo" in
match Coq_config.coqlib with
| Some coqlib when Sys.file_exists (coqlib / file) -> coqlib
| Some _ | None ->
let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
let prefix = Filename.dirname coqbin in
let rpath =
if Coq_config.local then []
else if Coq_config.arch_is_win32 then ["lib"]
else ["lib/coq"]
in
let coqlib = List.fold_left (/) prefix rpath in
if Sys.file_exists (coqlib / file) then coqlib
else prefix
let header_trailer = ref true
let header_file = ref ""
let header_file_spec = ref false
let footer_file = ref ""
let footer_file_spec = ref false
let quiet = ref true
let light = ref false
let gallina = ref false
let short = ref false
let index = ref true
let multi_index = ref false
let index_name = ref "index"
let toc = ref false
let page_title = ref ""
let title = ref ""
let externals = ref true
let coqlib = ref Coq_config.wwwstdlib
let coqlib_path = ref (guess_coqlib ())
let raw_comments = ref false
let parse_comments = ref false
let plain_comments = ref false
let toc_depth = (ref None : int option ref)
let lib_name = ref "Library"
let lib_subtitles = ref false
let interpolate = ref false
let inline_notmono = ref false
let charset = ref "iso-8859-1"
let inputenc = ref ""
let latin1 = ref false
let utf8 = ref false
let set_latin1 () =
charset := "iso-8859-1";
inputenc := "latin1";
latin1 := true
let set_utf8 () =
charset := "utf-8";
inputenc := "utf8x";
utf8 := true
(* Parsing options *)
type coq_module = string
type file =
| Vernac_file of string * coq_module
| Latex_file of string
|
