diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-29 11:59:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-29 11:59:13 +0000 |
| commit | 5893703b77fb17885fd66dbf575b9533cbf96a90 (patch) | |
| tree | c401c0607604b56a1360e4fdae3304d521c9bfe3 /tools/coqdoc/index.ml | |
| parent | 62ddbf4c06974bb701dd6b370c6b4d670cb5d7cd (diff) | |
Fixed broken globalization of identifiers containing utf8 letters
without knowing it.
Note: location tables have grown a lot, a better representation of the
contents of the glob files in coqdoc might improve efficiency.
Also added keywords.
Information is now obtained from the glob file to know the exact span
of identifiers. Kept a class of identifiers (and enriched them) for
the main purpose of distinguishing between idents and symbols in the
absence of a glob file.
Still a lot of work to do in coqdoc to make it more robust...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14624 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/index.ml')
| -rw-r--r-- | tools/coqdoc/index.ml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 2ff0fad70..c8e7770ae 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -58,8 +58,10 @@ let full_ident sp id = then id else "" -let add_def loc ty sp id = - Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty)); +let add_def loc1 loc2 ty sp id = + for loc = loc1 to loc2 do + Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty)) + done; Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty)) let add_ref m loc m' sp id ty = @@ -359,16 +361,16 @@ let read_glob vfile f = for loc=loc1 to loc2 do add_ref !cur_mod loc lib_dp sp id (type_of_string ty) done) - with _ -> - try - Scanf.sscanf s "R%d %s %s %s %s" - (fun loc lib_dp sp id ty -> - add_ref !cur_mod loc lib_dp sp id (type_of_string ty)) with _ -> ()) | _ -> - try Scanf.sscanf s "%s %d %s %s" - (fun ty loc sp id -> add_def loc (type_of_string ty) sp id) + try Scanf.sscanf s "not %d %s %s" + (fun loc sp id -> add_def loc loc (type_of_string "not") sp id) + with Scanf.Scan_failure _ -> + try Scanf.sscanf s "%s %d:%d %s %s" + (fun ty loc1 loc2 sp id -> + add_def loc1 loc2 (type_of_string ty) sp id) with Scanf.Scan_failure _ -> () + end done; assert false with End_of_file -> |