From f50e6f8daa9bf2a77fb0f7eaebf5426a8b7f7b12 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Mon, 1 Sep 2014 15:38:39 +0200 Subject: [PATCH] why3doc: fixed references to local files --- src/why3doc/doc_def.ml | 8 ++++++-- src/why3doc/doc_def.mli | 2 ++ src/why3doc/doc_main.ml | 2 +- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/why3doc/doc_def.ml b/src/why3doc/doc_def.ml index 889262f4f..faee1c9b6 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 d081dbf18..7fc84aad5 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 0be76caa5..d59a86f2b 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 *) -- GitLab