aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-10-27 18:00:59 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-10-27 18:00:59 +0000
commit2b1e771f49be6794bbe7e7d2f54b7571ccdf35b3 (patch)
tree3a8f963f7046bc5846a07aee3994d91db9847d28
parent05f7d5c2564bb10fa09853b088aac1b063496c6e (diff)
Added option --external to coqdoc to bind an url to an external library.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12426 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--CHANGES1
-rw-r--r--man/coqdoc.14
-rw-r--r--tools/coqdoc/index.mli6
-rw-r--r--tools/coqdoc/index.mll25
-rw-r--r--tools/coqdoc/main.ml4
-rw-r--r--tools/coqdoc/output.ml22
6 files changed, 43 insertions, 19 deletions
diff --git a/CHANGES b/CHANGES
index 681bd791d..84e9e8bfe 100644
--- a/CHANGES
+++ b/CHANGES
@@ -83,6 +83,7 @@ Coqdoc
- New option "--plain-comments" to disable interpretation inside comments.
- New option "--interpolate" to try and typeset identifiers in Coq escapings
using the available globalization information.
+- New option "--external url root" to refer to external libraries.
Library
diff --git a/man/coqdoc.1 b/man/coqdoc.1
index 45fcafd24..1b4cb7b6f 100644
--- a/man/coqdoc.1
+++ b/man/coqdoc.1
@@ -121,6 +121,10 @@ globalizations are obtained with Coq option \-dump\-glob).
Do not insert links to the Coq standard library.
.TP
+.BI \-\-external \ url \ libroot
+Set base URL for the external library whose root prefix is libroot.
+
+.TP
.BI \-\-coqlib \ url
Set base URL for the Coq standard library (default is http://coq.inria.fr/library/).
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index f8a8730d0..3649d6a4a 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -44,10 +44,14 @@ val find_string : coq_module -> string -> index_entry
val add_module : coq_module -> unit
-type module_kind = Local | Coqlib | Unknown
+type module_kind = Local | External of coq_module | Unknown
val find_module : coq_module -> module_kind
+val init_coqlib_library : unit -> unit
+
+val add_external_library : string -> coq_module -> unit
+
(*s Scan identifiers introductions from a file *)
val scan_file : string -> coq_module -> unit
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index a39450986..7f770f0f5 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -150,17 +150,32 @@ let add_module m =
Hashtbl.add modules id m;
Hashtbl.add local_modules m ()
-type module_kind = Local | Coqlib | Unknown
+type module_kind = Local | External of string | Unknown
-let coq_module m = String.length m >= 4 && String.sub m 0 4 = "Coq."
+let external_libraries = ref []
+
+let add_external_library logicalpath url =
+ external_libraries := (logicalpath,url) :: !external_libraries
+
+let find_external_library logicalpath =
+ let rec aux = function
+ | [] -> raise Not_found
+ | (l,u)::rest ->
+ Printf.eprintf "Looking for %s in %s\n%!" l logicalpath;
+ if String.length logicalpath > String.length l &
+ String.sub logicalpath 0 (String.length l + 1) = l ^"."
+ then u
+ else aux rest
+ in aux !external_libraries
+
+let init_coqlib_library () = add_external_library "Coq" !coqlib
let find_module m =
if Hashtbl.mem local_modules m then
Local
- else if coq_module m then
- Coqlib
else
- Unknown
+ try External (Filename.concat (find_external_library m) m)
+ with Not_found -> Unknown
(* Building indexes *)
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index d2b66f993..7fb9322d7 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -56,6 +56,7 @@ let usage () =
prerr_endline " --quiet quiet mode (default)";
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";
@@ -349,6 +350,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") :: [] ->
@@ -568,6 +571,7 @@ 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
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 0c5e9ff29..1d68b010e 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -256,10 +256,9 @@ module Latex = struct
match find_module m with
| Local ->
printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
- | Coqlib when !externals ->
- let m = Filename.concat !coqlib m in
+ | External m when !externals ->
printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
- | Coqlib | Unknown ->
+ | External _ | Unknown ->
raw_ident s
i*)
@@ -268,10 +267,9 @@ module Latex = struct
match find_module m with
| Local ->
printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
- | Coqlib when !externals ->
- let _m = Filename.concat !coqlib m in
- printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
- | Coqlib | Unknown ->
+ | External _ when !externals ->
+ printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
+ | External _ | Unknown ->
printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
let defref m id ty s =
@@ -481,10 +479,9 @@ module Html = struct
match find_module m with
| Local ->
printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
- | Coqlib when !externals ->
- let m = Filename.concat !coqlib m in
+ | External m when !externals ->
printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
- | Coqlib | Unknown ->
+ | External _ | Unknown ->
raw_ident s
let ident_ref m fid typ s =
@@ -494,12 +491,11 @@ module Html = struct
printf "<span class=\"id\" type=\"%s\">" typ;
raw_ident s;
printf "</span></a>"
- | Coqlib when !externals ->
- let m = Filename.concat !coqlib m in
+ | External m when !externals ->
printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
printf "<span class=\"id\" type=\"%s\">" typ;
raw_ident s; printf "</span></a>"
- | Coqlib | Unknown ->
+ | External _ | Unknown ->
printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>"
let reference s r =