summaryrefslogtreecommitdiff
path: root/tools/coqdoc/cdglobals.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/cdglobals.ml')
-rw-r--r--tools/coqdoc/cdglobals.ml46
1 files changed, 33 insertions, 13 deletions
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5cb670dc..f37db46b 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <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 *)
@@ -49,21 +49,40 @@ type glob_source_t =
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 = "states/initial.coq" in
- if Sys.file_exists (Filename.concat Coq_config.coqlib file)
- then Coq_config.coqlib
- else
- let coqbin = Filename.dirname Sys.executable_name in
- let prefix = Filename.dirname coqbin in
- let rpath = if Coq_config.local then [] else
- (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
- let coqlib = List.fold_left Filename.concat prefix rpath in
- if Sys.file_exists (Filename.concat coqlib file) then coqlib
- else
- Coq_config.coqlib
+ match Coq_config.coqlib with
+ | Some coqlib when Sys.file_exists (Filename.concat 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 = "win32" then ["lib"] else ["lib";"coq"]) in
+ let coqlib = List.fold_left Filename.concat prefix rpath in
+ if Sys.file_exists (Filename.concat coqlib file) then coqlib
+ else prefix
let header_trailer = ref true
let header_file = ref ""
@@ -90,6 +109,7 @@ 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 ""
@@ -103,7 +123,7 @@ let set_latin1 () =
let set_utf8 () =
charset := "utf-8";
- inputenc := "utf8";
+ inputenc := "utf8x";
utf8 := true
(* Parsing options *)