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

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 =