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

4 files changed, 33 insertions, 20 deletions

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 4a8756b88..07e813e74 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -123,9 +123,14 @@ let remove_sections dir =
     (* Theorem/Lemma outside its outer section of definition *)
     dir
 
+let interval loc =
+  let loc1,loc2 = Util.unloc loc in
+  loc1, loc2-1
+
 let dump_ref loc filepath modpath ident ty =
-  dump_string (Printf.sprintf "R%d %s %s %s %s\n"
-		  (fst (Util.unloc loc)) filepath modpath ident ty)
+  let bl,el = interval loc in
+  dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
+		  bl el filepath modpath ident ty)
 
 let add_glob_gen loc sp lib_dp ty =
   if dump () then
@@ -157,12 +162,14 @@ let add_glob_kn loc kn =
 let dump_binding loc id = ()
 
 let dump_definition (loc, id) sec s =
-  dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc))
+  let bl,el = interval loc in
+  dump_string (Printf.sprintf "%s %d:%d %s %s\n" s bl el
 			(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))
 
 let dump_reference loc modpath ident ty =
-  dump_string (Printf.sprintf "R%d %s %s %s %s\n"
-		  (fst (Util.unloc loc)) (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
+  let bl,el = interval loc in
+  dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
+		  bl el (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
 
 let dump_constraint ((loc, n), _, _) sec ty =
   match n with
@@ -175,18 +182,21 @@ let dump_modref loc mp ty =
     let l = if l = [] then l else Util.list_drop_last l in
     let fp = Names.string_of_dirpath dp in
     let mp = Names.string_of_dirpath (Names.make_dirpath l) in
-      dump_string (Printf.sprintf "R%d %s %s %s %s\n"
-		      (fst (Util.unloc loc)) fp mp "<>" ty)
+    let bl,el = interval loc in
+      dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
+		      bl el fp mp "<>" ty)
 
 let dump_moddef loc mp ty =
   if dump () then
+    let bl,el = interval loc in
     let (dp, l) = Lib.split_modpath mp in
     let mp = Names.string_of_dirpath (Names.make_dirpath l) in
-      dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
+      dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el "<>" mp)
 
 let dump_libref loc dp ty =
-  dump_string (Printf.sprintf "R%d %s <> <> %s\n"
-		  (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
+  let bl,el = interval loc in
+  dump_string (Printf.sprintf "R%d:%d %s <> <> %s\n"
+		  bl el (Names.string_of_dirpath dp) ty)
 
 let cook_notation df sc =
   (* We encode notations so that they are space-free and still human-readable *)
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 65a232b4a..89047e83c 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -276,7 +276,7 @@ let firstchar =
   (* '\206' ([ '\145' - '\183'] | '\187') | *)
   (* '\xCF' [ '\x00' - '\xCE' ] |  *)
   (* utf-8 letterlike symbols *)
-  '\206' ('\160' | [ '\177'-'\183'] | '\187') |
+  '\206' (['\145'-'\161'] | ['\163'-'\187']) |
   '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
     | '\129' [ '\176'-'\187' ] (* superscripts *)
     | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
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 ->
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 28cd79968..e3d5741ac 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -45,6 +45,7 @@ let is_keyword =
       "Implicit Arguments"; "Add"; "Strict";
       "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
       "subgoal";
+      "Opaque"; "Transparent";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";