diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | man/coqdoc.1 | 4 | ||||
| -rw-r--r-- | tools/coqdoc/index.mli | 6 | ||||
| -rw-r--r-- | tools/coqdoc/index.mll | 25 | ||||
| -rw-r--r-- | tools/coqdoc/main.ml | 4 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 22 |
6 files changed, 43 insertions, 19 deletions
@@ -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 = |