Continuing r15885 fixing coqdoc index bugs introduced in r14624 and r15053.

Indeed r15885 still had problems (index contained referenced objects and not
only defined objects, sorry).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15893 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 13 deletions

diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index a39b787956..ba71785c8d 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -37,12 +37,13 @@ type index_entry =
 let current_library = ref ""
   (** refers to the file being parsed *)
 
-(** [deftable] stores only definitions and is used to build the index
-    and to interpolate idents inside comments, which are not
-    globalized otherwise. *)
-
+(** [deftable] stores only definitions and is used to build the index *)
 let deftable = Hashtbl.create 97
 
+(** [byidtable] is used to interpolate idents inside comments, which are not
+    globalized otherwise. *)
+let byidtable = Hashtbl.create 97
+
 (** [reftable] stores references and definitions *)
 let reftable = Hashtbl.create 97
 
@@ -56,21 +57,25 @@ let full_ident sp id =
   else ""
 
 let add_def loc1 loc2 ty sp id =
+  let fullid = full_ident sp id in
+  let def = Def (fullid, ty) in
   for loc = loc1 to loc2 do
-    Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty))
+    Hashtbl.add reftable (!current_library, loc) def
   done;
-  Hashtbl.add deftable id (!current_library, full_ident sp id, ty)
+  Hashtbl.add deftable !current_library (fullid, ty);
+  Hashtbl.add byidtable id (!current_library, fullid, ty)
 
 let add_ref m loc m' sp id ty =
+  let fullid = full_ident sp id in
   if Hashtbl.mem reftable (m, loc) then ()
-  else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty));
+  else Hashtbl.add reftable (m, loc) (Ref (m', fullid, ty));
   let idx = if id = "<>" then m' else id in
-    if Hashtbl.mem deftable idx then ()
-    else Hashtbl.add deftable idx (m', full_ident sp id, ty)
+    if Hashtbl.mem byidtable idx then ()
+    else Hashtbl.add byidtable idx (m', fullid, ty)
 
 let find m l = Hashtbl.find reftable (m, l)
 
-let find_string m s = let (m,s,t) = Hashtbl.find deftable s in Ref (m,s,t)
+let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
 
 (*s Manipulating path prefixes *)
 
@@ -254,9 +259,7 @@ let all_entries () =
     let l = try Hashtbl.find bt t with Not_found -> [] in
       Hashtbl.replace bt t ((s,m) :: l)
   in
-  let classify _ (m,s,t) =
-    if s <> "" && Hashtbl.mem local_modules m then (add_g s m t; add_bt t s m)
-  in
+  let classify m (s,t) = (add_g s m t; add_bt t s m) in
     Hashtbl.iter classify deftable;
     Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
     { idx_name = "global";