diff options
author | 2012-10-16 02:01:41 +0000 | |
---|---|---|
committer | 2012-10-16 02:01:41 +0000 | |
commit | 3b5927180128a4e8f10f7437641ff3af220194b3 (patch) | |
tree | 1717e4c1120329e7f7957ff7088292afcf39886b /tools | |
parent | a4b80ae55c5b1fc8b6c8ad5028a359cd6d5d6ce8 (diff) |
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
Diffstat (limited to 'tools')
-rw-r--r-- | tools/coqdoc/index.ml | 29 |
1 files changed, 16 insertions, 13 deletions
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index a39b78795..ba71785c8 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"; |