diff --git a/src/why3doc/doc_def.ml b/src/why3doc/doc_def.ml index 889262f4f032f910917e22b0d0647f8ad3262e0d..faee1c9b67671cfb4a1b5fb871951403e6dd4300 100644 --- a/src/why3doc/doc_def.ml +++ b/src/why3doc/doc_def.ml @@ -72,11 +72,15 @@ let tag_escape s = let make_tag s l = tag_escape s ^ "_" ^ string_of_int l +let local_files = Hashtbl.create 17 +let add_local_file fn = Hashtbl.add local_files (Filename.chop_extension fn) () +let is_local_file = Hashtbl.mem local_files + let make_url fn = let url = fn ^ ".html" in match !stdlib_url with - | None -> url - | Some www -> www ^ "/" ^ url + | Some www when not (is_local_file fn) -> www ^ "/" ^ url + | _ -> url let anchor id = match id.id_loc with | None -> raise Not_found diff --git a/src/why3doc/doc_def.mli b/src/why3doc/doc_def.mli index d081dbf185a9fd615241fc1ce9a519b41657dd28..7fc84aad5ed4fca8abee203048cbe7b693140ae2 100644 --- a/src/why3doc/doc_def.mli +++ b/src/why3doc/doc_def.mli @@ -12,6 +12,8 @@ open Why3 open Ident +val add_local_file: string -> unit + (* records definition locations *) val set_output_dir: string option -> unit diff --git a/src/why3doc/doc_main.ml b/src/why3doc/doc_main.ml index 0be76caa5099c9591a372c2e2f3e117d2a1825bb..d59a86f2bcfb7328b78f00bb962a408717037500 100644 --- a/src/why3doc/doc_main.ml +++ b/src/why3doc/doc_main.ml @@ -85,7 +85,7 @@ let print_file fname = close_out c let () = - (* Queue.iter Doc_def.add_file opt_queue; *) + Queue.iter Doc_def.add_local_file opt_queue; try Doc_def.set_output_dir !opt_output; (* process files *)